src/HOLCF/Porder.thy
 changeset 18088 e5b23b85e932 parent 18071 940c2c0ff33a child 18647 5f5d37e763c4
equal 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 *}`