diff -r 3a8d722fd3ff -r 16c4ea954511 Prod.ML --- a/Prod.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/Prod.ML Mon Nov 21 17:50:34 1994 +0100 @@ -11,52 +11,52 @@ (*This counts as a non-emptiness result for admitting 'a * 'b as a type*) goalw Prod.thy [Prod_def] "Pair_Rep(a,b) : Prod"; by (EVERY1 [rtac CollectI, rtac exI, rtac exI, rtac refl]); -val ProdI = result(); +qed "ProdI"; val [major] = goalw Prod.thy [Pair_Rep_def] "Pair_Rep(a, b) = Pair_Rep(a',b') ==> a=a' & b=b'"; by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), rtac conjI, rtac refl, rtac refl]); -val Pair_Rep_inject = result(); +qed "Pair_Rep_inject"; goal Prod.thy "inj_onto(Abs_Prod,Prod)"; by (rtac inj_onto_inverseI 1); by (etac Abs_Prod_inverse 1); -val inj_onto_Abs_Prod = result(); +qed "inj_onto_Abs_Prod"; val prems = goalw Prod.thy [Pair_def] "[| = ; [| a=a'; b=b' |] ==> R |] ==> R"; by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1); by (REPEAT (ares_tac (prems@[ProdI]) 1)); -val Pair_inject = result(); +qed "Pair_inject"; goal Prod.thy "( = ) = (a=a' & b=b')"; by (fast_tac (set_cs addIs [Pair_inject]) 1); -val Pair_eq = result(); +qed "Pair_eq"; goalw Prod.thy [fst_def] "fst() = a"; by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1); -val fst_conv = result(); +qed "fst_conv"; goalw Prod.thy [snd_def] "snd() = b"; by (fast_tac (set_cs addIs [select_equality] addSEs [Pair_inject]) 1); -val snd_conv = result(); +qed "snd_conv"; goalw Prod.thy [Pair_def] "? x y. p = "; by (rtac (rewrite_rule [Prod_def] Rep_Prod RS CollectE) 1); by (EVERY1[etac exE, etac exE, rtac exI, rtac exI, rtac (Rep_Prod_inverse RS sym RS trans), etac arg_cong]); -val PairE_lemma = result(); +qed "PairE_lemma"; val [prem] = goal Prod.thy "[| !!x y. p = ==> Q |] ==> Q"; by (rtac (PairE_lemma RS exE) 1); by (REPEAT (eresolve_tac [prem,exE] 1)); -val PairE = result(); +qed "PairE"; goalw Prod.thy [split_def] "split(c, ) = c(a,b)"; by (sstac [fst_conv, snd_conv] 1); by (rtac refl 1); -val split = result(); +qed "split"; val pair_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq]; @@ -64,7 +64,7 @@ by (res_inst_tac[("p","s")] PairE 1); by (res_inst_tac[("p","t")] PairE 1); by (asm_simp_tac pair_ss 1); -val Pair_fst_snd_eq = result(); +qed "Pair_fst_snd_eq"; (*Prevents simplification of c: much faster*) val split_weak_cong = prove_goal Prod.thy @@ -74,19 +74,19 @@ goal Prod.thy "p = "; by (res_inst_tac [("p","p")] PairE 1); by (asm_simp_tac pair_ss 1); -val surjective_pairing = result(); +qed "surjective_pairing"; goal Prod.thy "p = split(%x y., p)"; by (res_inst_tac [("p","p")] PairE 1); by (asm_simp_tac pair_ss 1); -val surjective_pairing2 = result(); +qed "surjective_pairing2"; (*For use with split_tac and the simplifier*) goal Prod.thy "R(split(c,p)) = (! x y. p = --> R(c(x,y)))"; by (stac surjective_pairing 1); by (stac split 1); by (fast_tac (HOL_cs addSEs [Pair_inject]) 1); -val expand_split = result(); +qed "expand_split"; (** split used as a logical connective or set former **) @@ -95,50 +95,50 @@ goal Prod.thy "!!a b c. c(a,b) ==> split(c, )"; by (asm_simp_tac pair_ss 1); -val splitI = result(); +qed "splitI"; val prems = goalw Prod.thy [split_def] "[| split(c,p); !!x y. [| p = ; c(x,y) |] ==> Q |] ==> Q"; by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); -val splitE = result(); +qed "splitE"; goal Prod.thy "!!R a b. split(R,) ==> R(a,b)"; by (etac (split RS iffD1) 1); -val splitD = result(); +qed "splitD"; goal Prod.thy "!!a b c. z: c(a,b) ==> z: split(c, )"; by (asm_simp_tac pair_ss 1); -val mem_splitI = result(); +qed "mem_splitI"; val prems = goalw Prod.thy [split_def] "[| z: split(c,p); !!x y. [| p = ; z: c(x,y) |] ==> Q |] ==> Q"; by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); -val mem_splitE = result(); +qed "mem_splitE"; (*** prod_fun -- action of the product functor upon functions ***) goalw Prod.thy [prod_fun_def] "prod_fun(f,g,) = "; by (rtac split 1); -val prod_fun = result(); +qed "prod_fun"; goal Prod.thy "prod_fun(f1 o f2, g1 o g2) = (prod_fun(f1,g1) o prod_fun(f2,g2))"; by (rtac ext 1); by (res_inst_tac [("p","x")] PairE 1); by (asm_simp_tac (pair_ss addsimps [prod_fun,o_def]) 1); -val prod_fun_compose = result(); +qed "prod_fun_compose"; goal Prod.thy "prod_fun(%x.x, %y.y) = (%z.z)"; by (rtac ext 1); by (res_inst_tac [("p","z")] PairE 1); by (asm_simp_tac (pair_ss addsimps [prod_fun]) 1); -val prod_fun_ident = result(); +qed "prod_fun_ident"; val prems = goal Prod.thy ":r ==> : prod_fun(f,g)``r"; by (rtac image_eqI 1); by (rtac (prod_fun RS sym) 1); by (resolve_tac prems 1); -val prod_fun_imageI = result(); +qed "prod_fun_imageI"; val major::prems = goal Prod.thy "[| c: prod_fun(f,g)``r; !!x y. [| c=; :r |] ==> P \ @@ -148,7 +148,7 @@ by (resolve_tac prems 1); by (fast_tac HOL_cs 2); by (fast_tac (HOL_cs addIs [prod_fun]) 1); -val prod_fun_imageE = result(); +qed "prod_fun_imageE"; (*** Disjoint union of a family of sets - Sigma ***) @@ -192,7 +192,7 @@ by (rtac bexI 1); by (rtac (fst_conv RS sym) 1); by (resolve_tac prems 1); -val fst_imageI = result(); +qed "fst_imageI"; val major::prems = goal Prod.thy "[| a : fst``r; !!y.[| : r |] ==> P |] ==> P"; @@ -201,7 +201,7 @@ by (etac ssubst 1); by (rtac (surjective_pairing RS subst) 1); by (assume_tac 1); -val fst_imageE = result(); +qed "fst_imageE"; (*** Range of a relation ***) @@ -210,7 +210,7 @@ by (rtac bexI 1); by (rtac (snd_conv RS sym) 1); by (resolve_tac prems 1); -val snd_imageI = result(); +qed "snd_imageI"; val major::prems = goal Prod.thy "[| a : snd``r; !!y.[| : r |] ==> P |] ==> P"; @@ -219,7 +219,7 @@ by (etac ssubst 1); by (rtac (surjective_pairing RS subst) 1); by (assume_tac 1); -val snd_imageE = result(); +qed "snd_imageE"; (** Exhaustion rule for unit -- a degenerate form of induction **) @@ -227,7 +227,7 @@ "u = Unity"; by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1); by (rtac (Rep_Unit_inverse RS sym) 1); -val unit_eq = result(); +qed "unit_eq"; val prod_cs = set_cs addSIs [SigmaI, mem_splitI] addIs [fst_imageI, snd_imageI, prod_fun_imageI]