# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265022406 -3600
# Node ID 9d5d9e7ff71b84b7855b188453e1630aab886db9
# Parent  44b013c59653c68d853ef0b2be1bcac0460422b8
Monotonicity of ~~gen, needed for using it in inductive definitions.

diff -r 44b013c59653 -r 9d5d9e7ff71b Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Mon Feb 01 11:39:59 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Mon Feb 01 12:06:46 2010 +0100
@@ -62,6 +62,9 @@
 notation
   alpha_gen ("_ \<approx>gen _ _ _ _")
 
+lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2"
+  by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps)
+
 lemma alpha_gen_refl:
   assumes a: "R x x"
   shows "(bs, x) \<approx>gen R f 0 (bs, x)"