--- a/src/HOL/Induct/LList.ML Thu Feb 01 20:51:13 2001 +0100
+++ b/src/HOL/Induct/LList.ML Thu Feb 01 20:51:48 2001 +0100
@@ -782,7 +782,7 @@
by (ALLGOALS Asm_simp_tac);
qed "fun_power_Suc";
-val Pair_cong = read_instantiate_sg (sign_of Product_Type.thy)
+val Pair_cong = read_instantiate_sg (sign_of (theory "Product_Type"))
[("f","Pair")] (standard(refl RS cong RS cong));
(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
--- a/src/HOL/Modelcheck/MuckeSyn.ML Thu Feb 01 20:51:13 2001 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.ML Thu Feb 01 20:51:48 2001 +0100
@@ -147,7 +147,7 @@
(* first simplification, then model checking *)
-goalw Product_Type.thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
+goalw (theory "Product_Type") [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
by (rtac ext 1);
by (stac (surjective_pairing RS sym) 1);
by (rtac refl 1);
--- a/src/HOL/Product_Type.thy Thu Feb 01 20:51:13 2001 +0100
+++ b/src/HOL/Product_Type.thy Thu Feb 01 20:51:48 2001 +0100
@@ -7,7 +7,11 @@
The unit type.
*)
-Product_Type = Fun +
+theory Product_Type = Fun
+files
+ ("Tools/split_rule.ML")
+ ("Product_Type_lemmas.ML")
+:
(** products **)
@@ -15,31 +19,34 @@
(* type definition *)
constdefs
- Pair_Rep :: ['a, 'b] => ['a, 'b] => bool
- "Pair_Rep == (%a b. %x y. x=a & y=b)"
+ Pair_Rep :: "['a, 'b] => ['a, 'b] => bool"
+ "Pair_Rep == (%a b. %x y. x=a & y=b)"
global
typedef (Prod)
('a, 'b) "*" (infixr 20)
= "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
+proof
+ fix a b show "Pair_Rep a b : ?Prod"
+ by blast
+qed
syntax (symbols)
- "*" :: [type, type] => type ("(_ \\<times>/ _)" [21, 20] 20)
-
+ "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
syntax (HTML output)
- "*" :: [type, type] => type ("(_ \\<times>/ _)" [21, 20] 20)
+ "*" :: "[type, type] => type" ("(_ \<times>/ _)" [21, 20] 20)
(* abstract constants and syntax *)
consts
- fst :: "'a * 'b => 'a"
- snd :: "'a * 'b => 'b"
- split :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
- prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
- Pair :: "['a, 'b] => 'a * 'b"
- Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set"
+ fst :: "'a * 'b => 'a"
+ snd :: "'a * 'b => 'b"
+ split :: "[['a, 'b] => 'c, 'a * 'b] => 'c"
+ prod_fun :: "['a => 'b, 'c => 'd, 'a * 'c] => 'b * 'd"
+ Pair :: "['a, 'b] => 'a * 'b"
+ Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set"
(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
@@ -51,11 +58,11 @@
"_tuple" :: "'a => tuple_args => 'a * 'b" ("(1'(_,/ _'))")
"_tuple_arg" :: "'a => tuple_args" ("_")
"_tuple_args" :: "'a => tuple_args => tuple_args" ("_,/ _")
- "_pattern" :: [pttrn, patterns] => pttrn ("'(_,/ _')")
- "" :: pttrn => patterns ("_")
- "_patterns" :: [pttrn, patterns] => patterns ("_,/ _")
- "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
- "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80)
+ "_pattern" :: "[pttrn, patterns] => pttrn" ("'(_,/ _')")
+ "" :: "pttrn => patterns" ("_")
+ "_patterns" :: "[pttrn, patterns] => patterns" ("_,/ _")
+ "@Sigma" ::"[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10)
+ "@Times" ::"['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80)
translations
"(x, y)" == "Pair x y"
@@ -70,8 +77,10 @@
"A <*> B" => "Sigma A (_K B)"
syntax (symbols)
- "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10)
- "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80)
+ "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\<Sigma> _\<in>_./ _)" 10)
+ "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \<times> _" [81, 80] 80)
+
+print_translation {* [("Sigma", dependent_tr' ("@Sigma", "@Times"))]; *}
(* definitions *)
@@ -79,12 +88,12 @@
local
defs
- Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)"
- fst_def "fst p == @a. ? b. p = (a, b)"
- snd_def "snd p == @b. ? a. p = (a, b)"
- split_def "split == (%c p. c (fst p) (snd p))"
- prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))"
- Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
+ Pair_def: "Pair a b == Abs_Prod(Pair_Rep a b)"
+ fst_def: "fst p == @a. ? b. p = (a, b)"
+ snd_def: "snd p == @b. ? a. p = (a, b)"
+ split_def: "split == (%c p. c (fst p) (snd p))"
+ prod_fun_def: "prod_fun f g == split(%x y.(f(x), g(y)))"
+ Sigma_def: "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
@@ -92,7 +101,11 @@
global
-typedef unit = "{True}"
+typedef unit = "{True}"
+proof
+ show "True : ?unit"
+ by blast
+qed
consts
"()" :: unit ("'(')")
@@ -100,10 +113,11 @@
local
defs
- Unity_def "() == Abs_unit True"
+ Unity_def: "() == Abs_unit True"
+
+use "Product_Type_lemmas.ML"
+
+use "Tools/split_rule.ML"
+setup split_attributes
end
-
-ML
-
-val print_translation = [("Sigma", dependent_tr' ("@Sigma", "@Times"))];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Product_Type_lemmas.ML Thu Feb 01 20:51:48 2001 +0100
@@ -0,0 +1,584 @@
+(* Title: HOL/Product_Type_lemmas.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1991 University of Cambridge
+
+Ordered Pairs, the Cartesian product type, the unit type
+*)
+
+(* ML bindings *)
+val Pair_def = thm "Pair_def";
+val fst_def = thm "fst_def";
+val snd_def = thm "snd_def";
+val split_def = thm "split_def";
+val prod_fun_def = thm "prod_fun_def";
+val Sigma_def = thm "Sigma_def";
+val Unity_def = thm "Unity_def";
+
+
+(** unit **)
+
+Goalw [Unity_def] "u = ()";
+by (stac (rewrite_rule [thm"unit_def"] (thm"Rep_unit") RS singletonD RS sym) 1);
+by (rtac (thm "Rep_unit_inverse" RS sym) 1);
+qed "unit_eq";
+
+(*simplification procedure for unit_eq.
+ Cannot use this rule directly -- it loops!*)
+local
+ val unit_pat = Thm.cterm_of (Theory.sign_of (the_context ())) (Free ("x", HOLogic.unitT));
+ val unit_meta_eq = standard (mk_meta_eq unit_eq);
+ fun proc _ _ t =
+ if HOLogic.is_unit t then None
+ else Some unit_meta_eq;
+in
+ val unit_eq_proc = Simplifier.mk_simproc "unit_eq" [unit_pat] proc;
+end;
+
+Addsimprocs [unit_eq_proc];
+
+Goal "(!!x::unit. PROP P x) == PROP P ()";
+by (Simp_tac 1);
+qed "unit_all_eq1";
+
+Goal "(!!x::unit. PROP P) == PROP P";
+by (rtac triv_forall_equality 1);
+qed "unit_all_eq2";
+
+Goal "P () ==> P x";
+by (Simp_tac 1);
+qed "unit_induct";
+
+(*This rewrite counters the effect of unit_eq_proc on (%u::unit. f u),
+ replacing it by f rather than by %u.f(). *)
+Goal "(%u::unit. f()) = f";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "unit_abs_eta_conv";
+Addsimps [unit_abs_eta_conv];
+
+
+(** prod **)
+
+Goalw [thm "Prod_def"] "Pair_Rep a b : Prod";
+by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]);
+qed "ProdI";
+
+Goalw [thm "Pair_Rep_def"] "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'";
+by (dtac (fun_cong RS fun_cong) 1);
+by (Blast_tac 1);
+qed "Pair_Rep_inject";
+
+Goal "inj_on Abs_Prod Prod";
+by (rtac inj_on_inverseI 1);
+by (etac (thm "Abs_Prod_inverse") 1);
+qed "inj_on_Abs_Prod";
+
+val prems = Goalw [Pair_def]
+ "[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R";
+by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
+by (REPEAT (ares_tac (prems@[ProdI]) 1));
+qed "Pair_inject";
+
+Goal "((a,b) = (a',b')) = (a=a' & b=b')";
+by (blast_tac (claset() addSEs [Pair_inject]) 1);
+qed "Pair_eq";
+AddIffs [Pair_eq];
+
+Goalw [fst_def] "fst (a,b) = a";
+by (Blast_tac 1);
+qed "fst_conv";
+Goalw [snd_def] "snd (a,b) = b";
+by (Blast_tac 1);
+qed "snd_conv";
+Addsimps [fst_conv, snd_conv];
+
+Goal "fst (x, y) = a ==> x = a";
+by (Asm_full_simp_tac 1);
+qed "fst_eqD";
+Goal "snd (x, y) = a ==> y = a";
+by (Asm_full_simp_tac 1);
+qed "snd_eqD";
+
+Goalw [Pair_def] "? x y. p = (x,y)";
+by (rtac (rewrite_rule [thm "Prod_def"] (thm "Rep_Prod") RS CollectE) 1);
+by (EVERY1[etac exE, etac exE, rtac exI, rtac exI,
+ rtac (thm "Rep_Prod_inverse" RS sym RS trans), etac arg_cong]);
+qed "PairE_lemma";
+
+val [prem] = Goal "[| !!x y. p = (x,y) ==> Q |] ==> Q";
+by (rtac (PairE_lemma RS exE) 1);
+by (REPEAT (eresolve_tac [prem,exE] 1));
+qed "PairE";
+
+fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac,
+ K prune_params_tac];
+
+(* Do not add as rewrite rule: invalidates some proofs in IMP *)
+Goal "p = (fst(p),snd(p))";
+by (pair_tac "p" 1);
+by (Asm_simp_tac 1);
+qed "surjective_pairing";
+Addsimps [surjective_pairing RS sym];
+
+Goal "? x y. z = (x, y)";
+by (rtac exI 1);
+by (rtac exI 1);
+by (rtac surjective_pairing 1);
+qed "surj_pair";
+Addsimps [surj_pair];
+
+
+bind_thm ("split_paired_all",
+ SplitPairedAll.rule (standard (surjective_pairing RS eq_reflection)));
+bind_thms ("split_tupled_all", [split_paired_all, unit_all_eq2]);
+
+(*
+Addsimps [split_paired_all] does not work with simplifier
+because it also affects premises in congrence rules,
+where is can lead to premises of the form !!a b. ... = ?P(a,b)
+which cannot be solved by reflexivity.
+*)
+
+(* replace parameters of product type by individual component parameters *)
+local
+ fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
+ can HOLogic.dest_prodT T orelse exists_paired_all t
+ | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u
+ | exists_paired_all (Abs (_, _, t)) = exists_paired_all t
+ | exists_paired_all _ = false;
+ val ss = HOL_basic_ss
+ addsimps [split_paired_all, unit_all_eq2, unit_abs_eta_conv]
+ addsimprocs [unit_eq_proc];
+in
+ val split_all_tac = SUBGOAL (fn (t, i) =>
+ if exists_paired_all t then full_simp_tac ss i else no_tac);
+ fun split_all th =
+ if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th;
+end;
+
+claset_ref() := claset()
+ addSWrapper ("split_all_tac", fn tac2 => split_all_tac ORELSE' tac2);
+
+Goal "(!x. P x) = (!a b. P(a,b))";
+by (Fast_tac 1);
+qed "split_paired_All";
+Addsimps [split_paired_All];
+(* AddIffs is not a good idea because it makes Blast_tac loop *)
+
+bind_thm ("prod_induct",
+ allI RS (allI RS (split_paired_All RS iffD2)) RS spec);
+
+Goal "(? x. P x) = (? a b. P(a,b))";
+by (Fast_tac 1);
+qed "split_paired_Ex";
+Addsimps [split_paired_Ex];
+
+Goalw [split_def] "split c (a,b) = c a b";
+by (Simp_tac 1);
+qed "split_conv";
+Addsimps [split_conv];
+(*bind_thm ("split", split_conv); (*for compatibility*)*)
+
+(*Subsumes the old split_Pair when f is the identity function*)
+Goal "split (%x y. f(x,y)) = f";
+by (rtac ext 1);
+by (pair_tac "x" 1);
+by (Simp_tac 1);
+qed "split_Pair_apply";
+
+(*Can't be added to simpset: loops!*)
+Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
+by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
+qed "split_paired_Eps";
+
+Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
+by (rtac refl 1);
+qed "Eps_split";
+
+Goal "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "Pair_fst_snd_eq";
+
+Goal "fst p = fst q ==> snd p = snd q ==> p = q";
+by (asm_simp_tac (simpset() addsimps [Pair_fst_snd_eq]) 1);
+qed "prod_eqI";
+AddXIs [prod_eqI];
+
+(*Prevents simplification of c: much faster*)
+Goal "p=q ==> split c p = split c q";
+by (etac arg_cong 1);
+qed "split_weak_cong";
+
+Goal "(%(x,y). f(x,y)) = f";
+by (rtac ext 1);
+by (split_all_tac 1);
+by (rtac split_conv 1);
+qed "split_eta";
+
+val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
+by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
+qed "cond_split_eta";
+
+(*simplification procedure for cond_split_eta.
+ using split_eta a rewrite rule is not general enough, and using
+ cond_split_eta directly would render some existing proofs very inefficient.
+ similarly for split_beta. *)
+local
+ fun Pair_pat k 0 (Bound m) = (m = k)
+ | Pair_pat k i (Const ("Pair", _) $ Bound m $ t) = i > 0 andalso
+ m = k+i andalso Pair_pat k (i-1) t
+ | Pair_pat _ _ _ = false;
+ fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
+ | no_args k i (t $ u) = no_args k i t andalso no_args k i u
+ | no_args k i (Bound m) = m < k orelse m > k+i
+ | no_args _ _ _ = true;
+ fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then Some (i,t) else None
+ | split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
+ | split_pat tp i _ = None;
+ fun metaeq sg lhs rhs = mk_meta_eq (prove_goalw_cterm []
+ (cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs))))
+ (K [simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1]));
+ val sign = sign_of (the_context ());
+ fun simproc name patstr = Simplifier.mk_simproc name
+ [Thm.read_cterm sign (patstr, HOLogic.termT)];
+
+ val beta_patstr = "split f z";
+ val eta_patstr = "split f";
+ fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
+ | beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
+ (beta_term_pat k i t andalso beta_term_pat k i u)
+ | beta_term_pat k i t = no_args k i t;
+ fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
+ | eta_term_pat _ _ _ = false;
+ fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
+ | subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
+ else (subst arg k i t $ subst arg k i u)
+ | subst arg k i t = t;
+ fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
+ (case split_pat beta_term_pat 1 t of
+ Some (i,f) => Some (metaeq sg s (subst arg 0 i f))
+ | None => None)
+ | beta_proc _ _ _ = None;
+ fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
+ (case split_pat eta_term_pat 1 t of
+ Some (_,ft) => Some (metaeq sg s (let val (f $ arg) = ft in f end))
+ | None => None)
+ | eta_proc _ _ _ = None;
+in
+ val split_beta_proc = simproc "split_beta" beta_patstr beta_proc;
+ val split_eta_proc = simproc "split_eta" eta_patstr eta_proc;
+end;
+
+Addsimprocs [split_beta_proc,split_eta_proc];
+
+Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
+by (stac surjective_pairing 1 THEN rtac split_conv 1);
+qed "split_beta";
+
+(*For use with split_tac and the simplifier*)
+Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
+by (stac surjective_pairing 1);
+by (stac split_conv 1);
+by (Blast_tac 1);
+qed "split_split";
+
+(* could be done after split_tac has been speeded up significantly:
+simpset_ref() := simpset() addsplits [split_split];
+ precompute the constants involved and don't do anything unless
+ the current goal contains one of those constants
+*)
+
+Goal "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
+by (stac split_split 1);
+by (Simp_tac 1);
+qed "split_split_asm";
+
+(** split used as a logical connective or set former **)
+
+(*These rules are for use with blast_tac.
+ Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
+
+Goal "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "splitI2";
+
+Goal "!!p. [| !!a b. (a,b)=p ==> c a b x |] ==> split c p x";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "splitI2'";
+
+Goal "c a b ==> split c (a,b)";
+by (Asm_simp_tac 1);
+qed "splitI";
+
+val prems = Goalw [split_def]
+ "[| split c p; !!x y. [| p = (x,y); c x y |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+qed "splitE";
+
+val prems = Goalw [split_def]
+ "[| split c p z; !!x y. [| p = (x,y); c x y z |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+qed "splitE'";
+
+val major::prems = Goal
+ "[| Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R \
+\ |] ==> R";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+by (rtac (split_beta RS subst) 1 THEN rtac major 1);
+qed "splitE2";
+
+Goal "split R (a,b) ==> R a b";
+by (etac (split_conv RS iffD1) 1);
+qed "splitD";
+
+Goal "z: c a b ==> z: split c (a,b)";
+by (Asm_simp_tac 1);
+qed "mem_splitI";
+
+Goal "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
+by (split_all_tac 1);
+by (Asm_simp_tac 1);
+qed "mem_splitI2";
+
+val prems = Goalw [split_def]
+ "[| z: split c p; !!x y. [| p = (x,y); z: c x y |] ==> Q |] ==> Q";
+by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
+qed "mem_splitE";
+
+AddSIs [splitI, splitI2, splitI2', mem_splitI, mem_splitI2];
+AddSEs [splitE, splitE', mem_splitE];
+
+Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P";
+by (rtac ext 1);
+by (Fast_tac 1);
+qed "split_eta_SetCompr";
+Addsimps [split_eta_SetCompr];
+
+Goal "(%u. ? x y. u = (x, y) & P x y) = split P";
+br ext 1;
+by (Fast_tac 1);
+qed "split_eta_SetCompr2";
+Addsimps [split_eta_SetCompr2];
+
+(* allows simplifications of nested splits in case of independent predicates *)
+Goal "(%(a,b). P & Q a b) = (%ab. P & split Q ab)";
+by (rtac ext 1);
+by (Blast_tac 1);
+qed "split_part";
+Addsimps [split_part];
+
+Goal "(@(x',y'). x = x' & y = y') = (x,y)";
+by (Blast_tac 1);
+qed "Eps_split_eq";
+Addsimps [Eps_split_eq];
+(*
+the following would be slightly more general,
+but cannot be used as rewrite rule:
+### Cannot add premise as rewrite rule because it contains (type) unknowns:
+### ?y = .x
+Goal "[| P y; !!x. P x ==> x = y |] ==> (@(x',y). x = x' & P y) = (x,y)";
+by (rtac some_equality 1);
+by ( Simp_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
+qed "Eps_split_eq";
+*)
+
+(*** prod_fun -- action of the product functor upon functions ***)
+
+Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
+by (rtac split_conv 1);
+qed "prod_fun";
+Addsimps [prod_fun];
+
+Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
+by (rtac ext 1);
+by (pair_tac "x" 1);
+by (Asm_simp_tac 1);
+qed "prod_fun_compose";
+
+Goal "prod_fun (%x. x) (%y. y) = (%z. z)";
+by (rtac ext 1);
+by (pair_tac "z" 1);
+by (Asm_simp_tac 1);
+qed "prod_fun_ident";
+Addsimps [prod_fun_ident];
+
+Goal "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)`r";
+by (rtac image_eqI 1);
+by (rtac (prod_fun RS sym) 1);
+by (assume_tac 1);
+qed "prod_fun_imageI";
+
+val major::prems = Goal
+ "[| c: (prod_fun f g)`r; !!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P \
+\ |] ==> P";
+by (rtac (major RS imageE) 1);
+by (res_inst_tac [("p","x")] PairE 1);
+by (resolve_tac prems 1);
+by (Blast_tac 2);
+by (blast_tac (claset() addIs [prod_fun]) 1);
+qed "prod_fun_imageE";
+
+AddIs [prod_fun_imageI];
+AddSEs [prod_fun_imageE];
+
+
+(*** Disjoint union of a family of sets - Sigma ***)
+
+Goalw [Sigma_def] "[| a:A; b:B(a) |] ==> (a,b) : Sigma A B";
+by (REPEAT (ares_tac [singletonI,UN_I] 1));
+qed "SigmaI";
+
+AddSIs [SigmaI];
+
+(*The general elimination rule*)
+val major::prems = Goalw [Sigma_def]
+ "[| c: Sigma A B; \
+\ !!x y.[| x:A; y:B(x); c=(x,y) |] ==> P \
+\ |] ==> P";
+by (cut_facts_tac [major] 1);
+by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
+qed "SigmaE";
+
+(** Elimination of (a,b):A*B -- introduces no eigenvariables **)
+
+Goal "(a,b) : Sigma A B ==> a : A";
+by (etac SigmaE 1);
+by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
+qed "SigmaD1";
+
+Goal "(a,b) : Sigma A B ==> b : B(a)";
+by (etac SigmaE 1);
+by (REPEAT (eresolve_tac [asm_rl,Pair_inject,ssubst] 1)) ;
+qed "SigmaD2";
+
+val [major,minor]= Goal
+ "[| (a,b) : Sigma A B; \
+\ [| a:A; b:B(a) |] ==> P \
+\ |] ==> P";
+by (rtac minor 1);
+by (rtac (major RS SigmaD1) 1);
+by (rtac (major RS SigmaD2) 1) ;
+qed "SigmaE2";
+
+AddSEs [SigmaE2, SigmaE];
+
+val prems = Goal
+ "[| A<=C; !!x. x:A ==> B x <= D x |] ==> Sigma A B <= Sigma C D";
+by (cut_facts_tac prems 1);
+by (blast_tac (claset() addIs (prems RL [subsetD])) 1);
+qed "Sigma_mono";
+
+Goal "Sigma {} B = {}";
+by (Blast_tac 1) ;
+qed "Sigma_empty1";
+
+Goal "A <*> {} = {}";
+by (Blast_tac 1) ;
+qed "Sigma_empty2";
+
+Addsimps [Sigma_empty1,Sigma_empty2];
+
+Goal "UNIV <*> UNIV = UNIV";
+by Auto_tac;
+qed "UNIV_Times_UNIV";
+Addsimps [UNIV_Times_UNIV];
+
+Goal "- (UNIV <*> A) = UNIV <*> (-A)";
+by Auto_tac;
+qed "Compl_Times_UNIV1";
+
+Goal "- (A <*> UNIV) = (-A) <*> UNIV";
+by Auto_tac;
+qed "Compl_Times_UNIV2";
+
+Addsimps [Compl_Times_UNIV1, Compl_Times_UNIV2];
+
+Goal "((a,b): Sigma A B) = (a:A & b:B(a))";
+by (Blast_tac 1);
+qed "mem_Sigma_iff";
+AddIffs [mem_Sigma_iff];
+
+Goal "x:C ==> (A <*> C <= B <*> C) = (A <= B)";
+by (Blast_tac 1);
+qed "Times_subset_cancel2";
+
+Goal "x:C ==> (A <*> C = B <*> C) = (A = B)";
+by (blast_tac (claset() addEs [equalityE]) 1);
+qed "Times_eq_cancel2";
+
+Goal "Collect (split (%x y. P x & Q x y)) = (SIGMA x:Collect P. Collect (Q x))";
+by (Fast_tac 1);
+qed "SetCompr_Sigma_eq";
+
+(*** Complex rules for Sigma ***)
+
+Goal "{(a,b). P a & Q b} = Collect P <*> Collect Q";
+by (Blast_tac 1);
+qed "Collect_split";
+
+Addsimps [Collect_split];
+
+(*Suggested by Pierre Chartier*)
+Goal "(UN (a,b):(A <*> B). E a <*> F b) = (UNION A E) <*> (UNION B F)";
+by (Blast_tac 1);
+qed "UN_Times_distrib";
+
+Goal "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))";
+by (Fast_tac 1);
+qed "split_paired_Ball_Sigma";
+Addsimps [split_paired_Ball_Sigma];
+
+Goal "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))";
+by (Fast_tac 1);
+qed "split_paired_Bex_Sigma";
+Addsimps [split_paired_Bex_Sigma];
+
+Goal "(SIGMA i:I Un J. C(i)) = (SIGMA i:I. C(i)) Un (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Un_distrib1";
+
+Goal "(SIGMA i:I. A(i) Un B(i)) = (SIGMA i:I. A(i)) Un (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Un_distrib2";
+
+Goal "(SIGMA i:I Int J. C(i)) = (SIGMA i:I. C(i)) Int (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Int_distrib1";
+
+Goal "(SIGMA i:I. A(i) Int B(i)) = (SIGMA i:I. A(i)) Int (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Int_distrib2";
+
+Goal "(SIGMA i:I - J. C(i)) = (SIGMA i:I. C(i)) - (SIGMA j:J. C(j))";
+by (Blast_tac 1);
+qed "Sigma_Diff_distrib1";
+
+Goal "(SIGMA i:I. A(i) - B(i)) = (SIGMA i:I. A(i)) - (SIGMA i:I. B(i))";
+by (Blast_tac 1);
+qed "Sigma_Diff_distrib2";
+
+Goal "Sigma (Union X) B = (UN A:X. Sigma A B)";
+by (Blast_tac 1);
+qed "Sigma_Union";
+
+(*Non-dependent versions are needed to avoid the need for higher-order
+ matching, especially when the rules are re-oriented*)
+Goal "(A Un B) <*> C = (A <*> C) Un (B <*> C)";
+by (Blast_tac 1);
+qed "Times_Un_distrib1";
+
+Goal "(A Int B) <*> C = (A <*> C) Int (B <*> C)";
+by (Blast_tac 1);
+qed "Times_Int_distrib1";
+
+Goal "(A - B) <*> C = (A <*> C) - (B <*> C)";
+by (Blast_tac 1);
+qed "Times_Diff_distrib1";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/split_rule.ML Thu Feb 01 20:51:48 2001 +0100
@@ -0,0 +1,95 @@
+(*Attempts to remove occurrences of split, and pair-valued parameters*)
+val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
+
+local
+
+(*In ap_split S T u, term u expects separate arguments for the factors of S,
+ with result type T. The call creates a new term expecting one argument
+ of type S.*)
+fun ap_split (Type ("*", [T1, T2])) T3 u =
+ HOLogic.split_const (T1, T2, T3) $
+ Abs("v", T1,
+ ap_split T2 T3
+ ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $
+ Bound 0))
+ | ap_split T T3 u = u;
+
+(*Curries any Var of function type in the rule*)
+fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2])), rl) =
+ let val T' = HOLogic.prodT_factors T1 ---> T2
+ val newt = ap_split T1 T2 (Var (v, T'))
+ val cterm = Thm.cterm_of (#sign (rep_thm rl))
+ in
+ instantiate ([], [(cterm t, cterm newt)]) rl
+ end
+ | split_rule_var' (t, rl) = rl;
+
+(*** Complete splitting of partially splitted rules ***)
+
+fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
+ (ap_split T (flat (map HOLogic.prodT_factors Ts) ---> U)
+ (incr_boundvars 1 u) $ Bound 0))
+ | ap_split' _ _ u = u;
+
+fun complete_split_rule_var ((t as Var (v, T), ts), (rl, vs)) =
+ let
+ val cterm = Thm.cterm_of (#sign (rep_thm rl))
+ val (Us', U') = strip_type T;
+ val Us = take (length ts, Us');
+ val U = drop (length ts, Us') ---> U';
+ val T' = flat (map HOLogic.prodT_factors Us) ---> U;
+ fun mk_tuple ((xs, insts), v as Var ((a, _), T)) =
+ let
+ val Ts = HOLogic.prodT_factors T;
+ val ys = variantlist (replicate (length Ts) a, xs);
+ in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
+ (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
+ end
+ | mk_tuple (x, _) = x;
+ val newt = ap_split' Us U (Var (v, T'));
+ val cterm = Thm.cterm_of (#sign (rep_thm rl));
+ val (vs', insts) = foldl mk_tuple ((vs, []), ts);
+ in
+ (instantiate ([], [(cterm t, cterm newt)] @ insts) rl, vs')
+ end
+ | complete_split_rule_var (_, x) = x;
+
+fun collect_vars (vs, Abs (_, _, t)) = collect_vars (vs, t)
+ | collect_vars (vs, t) = (case strip_comb t of
+ (v as Var _, ts) => (v, ts)::vs
+ | (t, ts) => foldl collect_vars (vs, ts));
+
+in
+
+val split_rule_var = standard o remove_split o split_rule_var';
+
+(*Curries ALL function variables occurring in a rule's conclusion*)
+fun split_rule rl = standard (remove_split (foldr split_rule_var' (term_vars (concl_of rl), rl)));
+
+fun complete_split_rule rl =
+ standard (remove_split (fst (foldr complete_split_rule_var
+ (collect_vars ([], concl_of rl),
+ (rl, map (fst o fst o dest_Var) (term_vars (#prop (rep_thm rl))))))))
+ |> RuleCases.save rl;
+
+end;
+fun complete_split x =
+ Attrib.no_args (Drule.rule_attribute (K complete_split_rule)) x;
+
+fun split_rule_goal xss rl = let
+ val ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
+ fun one_split i (th,s) = rule_by_tactic (pair_tac s i) th;
+ fun one_goal (xs,i) th = foldl (one_split i) (th,xs);
+ in standard (Simplifier.full_simplify ss (foldln one_goal xss rl))
+ |> RuleCases.save rl
+ end;
+fun split_format x =
+ Attrib.syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name))
+ >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x;
+
+val split_attributes = [Attrib.add_attributes
+ [("complete_split", (complete_split, complete_split),
+ "recursively split all pair-typed function arguments"),
+ ("split_format", (split_format, split_format),
+ "split given pair-typed subterms in premises")]];
+
--- a/src/HOL/ex/cla.ML Thu Feb 01 20:51:13 2001 +0100
+++ b/src/HOL/ex/cla.ML Thu Feb 01 20:51:48 2001 +0100
@@ -462,7 +462,8 @@
(*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
Fast_tac indeed copes!*)
-goal Product_Type.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
+goal (theory "Product_Type")
+ "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \
\ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) & J(x))";
by (Fast_tac 1);
@@ -470,7 +471,7 @@
(*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
It does seem obvious!*)
-goal Product_Type.thy
+goal (theory "Product_Type")
"(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \
\ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))";
@@ -488,7 +489,7 @@
by (Blast_tac 1);
result();
-goal Product_Type.thy
+goal (theory "Product_Type")
"(ALL x y. R(x,y) | R(y,x)) & \
\ (ALL x y. S(x,y) & S(y,x) --> x=y) & \
\ (ALL x y. R(x,y) --> S(x,y)) --> (ALL x y. S(x,y) --> R(x,y))";
--- a/src/HOLCF/Cprod1.ML Thu Feb 01 20:51:13 2001 +0100
+++ b/src/HOLCF/Cprod1.ML Thu Feb 01 20:51:48 2001 +0100
@@ -11,11 +11,12 @@
(* less_cprod is a partial order on 'a * 'b *)
(* ------------------------------------------------------------------------ *)
+(*###TO Product_Type_lemmas.ML *)
Goal "[|fst x = fst y; snd x = snd y|] ==> x = y";
by (subgoal_tac "(fst x,snd x)=(fst y,snd y)" 1);
by (rotate_tac ~1 1);
by (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing RS sym])1);
-by (asm_simp_tac (simpset_of Product_Type.thy) 1);
+by (asm_simp_tac (simpset_of (theory "Product_Type")) 1);
qed "Sel_injective_cprod";
Goalw [less_cprod_def] "(p::'a*'b) << p";