--- a/Sum.ML Thu Aug 18 11:40:54 1994 +0200
+++ b/Sum.ML Thu Aug 18 11:43:40 1994 +0200
@@ -1,9 +1,9 @@
-(* Title: HOL/sum
+(* Title: HOL/Sum.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-For sum.ML. The disjoint sum of two types
+For Sum.thy. The disjoint sum of two types
*)
open Sum;
@@ -43,6 +43,15 @@
val Inl_neq_Inr = standard (Inl_not_Inr RS notE);
val Inr_neq_Inl = sym RS Inl_neq_Inr;
+goal Sum.thy "(Inl(a)=Inr(b)) = False";
+by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1);
+val Inl_Inr_eq = result();
+
+goal Sum.thy "(Inr(b)=Inl(a)) = False";
+by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1);
+val Inr_Inl_eq = result();
+
+
(** Injectiveness of Inl and Inr **)
val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
@@ -72,29 +81,25 @@
val Inr_inject = inj_Inr RS injD;
goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
-br iffI 1;
-be (rewrite_rule [inj_def] Inl_inject) 1;
-be ssubst 1;
-br refl 1;
-val Inl_inj = result();
+by (fast_tac (HOL_cs addSEs [Inl_inject]) 1);
+val Inl_eq = result();
goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
-br iffI 1;
-be (rewrite_rule [inj_def] Inr_inject) 1;
-be ssubst 1;
-br refl 1;
-val Inr_inj = result();
+by (fast_tac (HOL_cs addSEs [Inr_inject]) 1);
+val Inr_eq = result();
+
+val sum_cs = set_cs addSEs [Inl_neq_Inr, Inr_neq_Inl]
+ addSDs [Inl_inject, Inr_inject];
+
(** sum_case -- the selection operator for sums **)
-goalw Sum.thy [sum_case_def] "sum_case(Inl(x), f, g) = f(x)";
-by (fast_tac (set_cs addIs [select_equality]
- addSEs [make_elim Inl_inject, Inl_neq_Inr]) 1);
+goalw Sum.thy [sum_case_def] "sum_case(f, g, Inl(x)) = f(x)";
+by (fast_tac (sum_cs addIs [select_equality]) 1);
val sum_case_Inl = result();
-goalw Sum.thy [sum_case_def] "sum_case(Inr(x), f, g) = g(x)";
-by (fast_tac (set_cs addIs [select_equality]
- addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
+goalw Sum.thy [sum_case_def] "sum_case(f, g, Inr(x)) = g(x)";
+by (fast_tac (sum_cs addIs [select_equality]) 1);
val sum_case_Inr = result();
(** Exhaustion rule for sums -- a degenerate form of induction **)
@@ -109,13 +114,13 @@
rtac (Rep_Sum_inverse RS sym)]));
val sumE = result();
-goal Sum.thy "sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)";
+goal Sum.thy "sum_case(%x::'a. f(Inl(x)), %y::'b. f(Inr(y)), s) = f(s)";
by (EVERY1 [res_inst_tac [("s","s")] sumE,
etac ssubst, rtac sum_case_Inl,
etac ssubst, rtac sum_case_Inr]);
val surjective_sum = result();
-goal Sum.thy "R(sum_case(s,f,g)) = \
+goal Sum.thy "R(sum_case(f,g,s)) = \
\ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
by (rtac sumE 1);
by (etac ssubst 1);
@@ -126,9 +131,46 @@
by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
val expand_sum_case = result();
-val sum_ss = pair_ss addsimps [sum_case_Inl, sum_case_Inr];
+val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,
+ sum_case_Inl, sum_case_Inr];
(*Prevents simplification of f and g: much faster*)
val sum_case_weak_cong = prove_goal Sum.thy
- "s=t ==> sum_case(s,f,g) = sum_case(t,f,g)"
+ "s=t ==> sum_case(f,g,s) = sum_case(f,g,t)"
(fn [prem] => [rtac (prem RS arg_cong) 1]);
+
+
+(** Rules for the Part primitive **)
+
+goalw Sum.thy [Part_def]
+ "!!a b A h. [| a : A; a=h(b) |] ==> a : Part(A,h)";
+by (fast_tac set_cs 1);
+val Part_eqI = result();
+
+val PartI = refl RSN (2,Part_eqI);
+
+val major::prems = goalw Sum.thy [Part_def]
+ "[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \
+\ |] ==> P";
+by (rtac (major RS IntE) 1);
+by (etac CollectE 1);
+by (etac exE 1);
+by (REPEAT (ares_tac prems 1));
+val PartE = result();
+
+goalw Sum.thy [Part_def] "Part(A,h) <= A";
+by (rtac Int_lower1 1);
+val Part_subset = result();
+
+goal Sum.thy "!!A B. A<=B ==> Part(A,h) <= Part(B,h)";
+by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
+val Part_mono = result();
+
+goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
+by (etac IntD1 1);
+val PartD1 = result();
+
+goal Sum.thy "Part(A,%x.x) = A";
+by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+val Part_id = result();
+