src/HOL/Partial_Function.thy
changeset 40288 520199d8b66e
parent 40252 029400b6c893
child 42949 618adb3584e5
     1.1 --- a/src/HOL/Partial_Function.thy	Fri Oct 29 18:17:11 2010 +0200
     1.2 +++ b/src/HOL/Partial_Function.thy	Fri Oct 29 21:41:14 2010 +0200
     1.3 @@ -26,6 +26,11 @@
     1.4  lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)"
     1.5  by (rule monotoneI) (auto simp: fun_ord_def)
     1.6  
     1.7 +lemma let_mono[partial_function_mono]:
     1.8 +  "(\<And>x. monotone orda ordb (\<lambda>f. b f x))
     1.9 +  \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))"
    1.10 +by (simp add: Let_def)
    1.11 +
    1.12  lemma if_mono[partial_function_mono]: "monotone orda ordb F 
    1.13  \<Longrightarrow> monotone orda ordb G
    1.14  \<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)"