# HG changeset patch
# User Andreas Lochbihler
# Date 1423659531 -3600
# Node ID d92b74f3f6e372bc3af620e98bd6a84a3e6625ed
# Parent  28e1349eb48b05fff9f258657c990fe8d2b37f37
add parametricity rules for monotone, fun_lub, and fun_ord

diff -r 28e1349eb48b -r d92b74f3f6e3 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Feb 11 13:52:12 2015 +0100
+++ b/src/HOL/List.thy	Wed Feb 11 13:58:51 2015 +0100
@@ -6795,6 +6795,21 @@
   shows "(rel_set (rel_prod A A) ===> rel_set (rel_prod A A)) rtrancl rtrancl"
 unfolding rtrancl_def by transfer_prover
 
+lemma monotone_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_total A"
+  shows "((A ===> A ===> op =) ===> (B ===> B ===> op =) ===> (A ===> B) ===> op =) monotone monotone"
+unfolding monotone_def[abs_def] by transfer_prover
+
+lemma fun_ord_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_total C"
+  shows "((A ===> B ===> op =) ===> (C ===> A) ===> (C ===> B) ===> op =) fun_ord fun_ord"
+unfolding fun_ord_def[abs_def] by transfer_prover
+
+lemma fun_lub_parametric [transfer_rule]:
+  assumes [transfer_rule]: "bi_total A"  "bi_unique A"
+  shows "((rel_set A ===> B) ===> rel_set (C ===> A) ===> C ===> B) fun_lub fun_lub"
+unfolding fun_lub_def[abs_def] by transfer_prover
+
 end
 
 end