# HG changeset patch
# User paulson
# Date 861357164 -7200
# Node ID 824e18a114c9d0f7ec434f5759b8c1d4cff20903
# Parent  b1a5455f0332978f6b59247be3e33f3a21b4ca4a
New monotonicity theorems

diff -r b1a5455f0332 -r 824e18a114c9 src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Fri Apr 18 11:52:19 1997 +0200
+++ b/src/HOL/ex/LList.ML	Fri Apr 18 11:52:44 1997 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/llist
+(*  Title:      HOL/ex/LList
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
@@ -188,10 +188,15 @@
 by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1);
 qed "LListD_subset_diag";
 
+
 (** Coinduction, using LListD_Fun
     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
  **)
 
+goalw thy [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
+by (REPEAT (ares_tac basic_monos 1));
+qed "LListD_Fun_mono";
+
 goalw LList.thy [LListD_Fun_def]
     "!!M. [| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
 by (etac LListD.coinduct 1);
@@ -640,6 +645,15 @@
 by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
 qed "prod_fun_range_eq_diag";
 
+(*Surprisingly hard to prove.  Used with lfilter*)
+goalw thy [llistD_Fun_def, prod_fun_def]
+    "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
+by (Auto_tac());
+br image_eqI 1;
+by (fast_tac (!claset addss (!simpset)) 1);
+by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
+qed "llistD_Fun_mono";
+
 (** To show two llists are equal, exhibit a bisimulation! 
       [also admits true equality] **)
 val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]