diff -r d9527f97246e -r 89669c58e506 mono.ML --- a/mono.ML Thu Aug 25 10:47:33 1994 +0200 +++ b/mono.ML Thu Aug 25 11:01:45 1994 +0200 @@ -6,15 +6,14 @@ Monotonicity of various operations *) -val [prem] = goal Set.thy - "[| !!x. P(x) ==> Q(x) |] ==> Collect(P) <= Collect(Q)"; -by (fast_tac (set_cs addIs [prem]) 1); -val Collect_mono = result(); - goal Set.thy "!!A B. A<=B ==> f``A <= f``B"; by (fast_tac set_cs 1); val image_mono = result(); +goal Set.thy "!!A B. A<=B ==> Pow(A) <= Pow(B)"; +by (fast_tac set_cs 1); +val Pow_mono = result(); + goal Set.thy "!!A B. A<=B ==> Union(A) <= Union(B)"; by (fast_tac set_cs 1); val Union_mono = result(); @@ -70,3 +69,55 @@ addSEs [SigmaE]) 1); val Sigma_mono = result(); + +(** Monotonicity of implications. For inductive definitions **) + +goal Set.thy "!!A B x. A<=B ==> x:A --> x:B"; +by (rtac impI 1); +by (etac subsetD 1); +by (assume_tac 1); +val in_mono = result(); + +goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"; +by (fast_tac HOL_cs 1); +val conj_mono = result(); + +goal HOL.thy "!!P1 P2 Q1 Q2. [| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"; +by (fast_tac HOL_cs 1); +val disj_mono = result(); + +goal HOL.thy "!!P1 P2 Q1 Q2.[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"; +by (fast_tac HOL_cs 1); +val imp_mono = result(); + +goal HOL.thy "P-->P"; +by (rtac impI 1); +by (assume_tac 1); +val imp_refl = result(); + +val [PQimp] = goal HOL.thy + "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))"; +by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1); +val ex_mono = result(); + +val [PQimp] = goal HOL.thy + "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))"; +by (fast_tac (HOL_cs addIs [PQimp RS mp]) 1); +val all_mono = result(); + +val [PQimp] = goal Set.thy + "[| !!x. P(x) --> Q(x) |] ==> Collect(P) <= Collect(Q)"; +by (fast_tac (set_cs addIs [PQimp RS mp]) 1); +val Collect_mono = result(); + +(*Used in indrule.ML*) +val [subs,PQimp] = goal Set.thy + "[| A<=B; !!x. x:A ==> P(x) --> Q(x) \ +\ |] ==> A Int Collect(P) <= B Int Collect(Q)"; +by (fast_tac (set_cs addIs [subs RS subsetD, PQimp RS mp]) 1); +val Int_Collect_mono = result(); + +(*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]; +