src/HOLCF/Porder.thy
changeset 18088 e5b23b85e932
parent 18071 940c2c0ff33a
child 18647 5f5d37e763c4
equal deleted inserted replaced
18087:577d57e51f89 18088:e5b23b85e932
    36 
    36 
    37 lemma antisym_less_inverse: "(x::'a::po) = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
    37 lemma antisym_less_inverse: "(x::'a::po) = y \<Longrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
    38 by simp
    38 by simp
    39 
    39 
    40 lemma box_less: "\<lbrakk>(a::'a::po) \<sqsubseteq> b; c \<sqsubseteq> a; b \<sqsubseteq> d\<rbrakk> \<Longrightarrow> c \<sqsubseteq> d"
    40 lemma box_less: "\<lbrakk>(a::'a::po) \<sqsubseteq> b; c \<sqsubseteq> a; b \<sqsubseteq> d\<rbrakk> \<Longrightarrow> c \<sqsubseteq> d"
    41 apply (erule trans_less)
    41 by (rule trans_less [OF trans_less])
    42 apply (erule trans_less)
       
    43 apply assumption
       
    44 done
       
    45 
    42 
    46 lemma po_eq_conv: "((x::'a::po) = y) = (x \<sqsubseteq> y \<and> y \<sqsubseteq> x)"
    43 lemma po_eq_conv: "((x::'a::po) = y) = (x \<sqsubseteq> y \<and> y \<sqsubseteq> x)"
    47 by (fast elim!: antisym_less_inverse intro!: antisym_less)
    44 by (fast elim!: antisym_less_inverse intro!: antisym_less)
    48 
    45 
    49 lemma rev_trans_less: "\<lbrakk>(y::'a::po) \<sqsubseteq> z; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    46 lemma rev_trans_less: "\<lbrakk>(y::'a::po) \<sqsubseteq> z; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
   126 apply assumption
   123 apply assumption
   127 apply (erule (1) unique_lub)
   124 apply (erule (1) unique_lub)
   128 done
   125 done
   129 
   126 
   130 lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
   127 lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
   131 apply (rule unique_lub)
   128 by (rule unique_lub [OF lubI])
   132 apply (rule lubI)
       
   133 apply assumption
       
   134 apply assumption
       
   135 done
       
   136 
   129 
   137 lemma lub_singleton [simp]: "lub {x} = x"
   130 lemma lub_singleton [simp]: "lub {x} = x"
   138 by (simp add: thelubI is_lub_def is_ub_def)
   131 by (simp add: thelubI is_lub_def is_ub_def)
   139 
   132 
   140 text {* access to some definition as inference rule *}
   133 text {* access to some definition as inference rule *}