huffman@15600: (* Title: HOLCF/Porder.thy nipkow@243: ID: $Id$ clasohm@1479: Author: Franz Regensburger nipkow@243: *) nipkow@243: huffman@15587: header {* Partial orders *} huffman@15576: huffman@15577: theory Porder huffman@19621: imports Finite_Set huffman@15577: begin huffman@15576: huffman@15587: subsection {* Type class for partial orders *} huffman@15587: huffman@23284: class sq_ord = type + huffman@23284: fixes sq_le :: "'a \ 'a \ bool" huffman@15576: huffman@23284: notation huffman@23284: sq_le (infixl "<<" 55) huffman@15576: huffman@23284: notation (xsymbols) huffman@23284: sq_le (infixl "\" 55) huffman@15576: huffman@15576: axclass po < sq_ord huffman@23284: refl_less [iff]: "x \ x" huffman@17810: antisym_less: "\x \ y; y \ x\ \ x = y" huffman@17810: trans_less: "\x \ y; y \ z\ \ x \ z" huffman@15576: huffman@15576: text {* minimal fixes least element *} huffman@15576: huffman@17810: lemma minimal2UU[OF allI] : "\x::'a::po. uu \ x \ uu = (THE u. \y. u \ y)" huffman@15930: by (blast intro: theI2 antisym_less) huffman@15576: huffman@15576: text {* the reverse law of anti-symmetry of @{term "op <<"} *} huffman@15576: huffman@17810: lemma antisym_less_inverse: "(x::'a::po) = y \ x \ y \ y \ x" huffman@17810: by simp huffman@15576: huffman@17810: lemma box_less: "\(a::'a::po) \ b; c \ a; b \ d\ \ c \ d" huffman@18088: by (rule trans_less [OF trans_less]) huffman@15576: huffman@17810: lemma po_eq_conv: "((x::'a::po) = y) = (x \ y \ y \ x)" huffman@17810: by (fast elim!: antisym_less_inverse intro!: antisym_less) huffman@17810: huffman@17810: lemma rev_trans_less: "\(y::'a::po) \ z; x \ y\ \ x \ z" huffman@17810: by (rule trans_less) huffman@15576: huffman@18647: lemma sq_ord_less_eq_trans: "\a \ b; b = c\ \ a \ c" huffman@18647: by (rule subst) huffman@18647: huffman@18647: lemma sq_ord_eq_less_trans: "\a = b; b \ c\ \ a \ c" huffman@18647: by (rule ssubst) huffman@18647: huffman@18647: lemmas HOLCF_trans_rules [trans] = huffman@18647: trans_less huffman@18647: antisym_less huffman@18647: sq_ord_less_eq_trans huffman@18647: sq_ord_eq_less_trans huffman@18647: huffman@15587: subsection {* Chains and least upper bounds *} nipkow@243: huffman@18071: constdefs huffman@18071: huffman@18071: -- {* class definitions *} huffman@18071: is_ub :: "['a set, 'a::po] \ bool" (infixl "<|" 55) huffman@18071: "S <| x \ \y. y \ S \ y \ x" huffman@18071: huffman@18071: is_lub :: "['a set, 'a::po] \ bool" (infixl "<<|" 55) huffman@18071: "S <<| x \ S <| x \ (\u. S <| u \ x \ u)" huffman@18071: huffman@18071: -- {* Arbitrary chains are total orders *} huffman@18071: tord :: "'a::po set \ bool" huffman@18071: "tord S \ \x y. x \ S \ y \ S \ (x \ y \ y \ x)" huffman@18071: huffman@18071: -- {* Here we use countable chains and I prefer to code them as functions! *} huffman@18071: chain :: "(nat \ 'a::po) \ bool" huffman@18071: "chain F \ \i. F i \ F (Suc i)" huffman@18071: huffman@18071: -- {* finite chains, needed for monotony of continuous functions *} huffman@18071: max_in_chain :: "[nat, nat \ 'a::po] \ bool" huffman@18071: "max_in_chain i C \ \j. i \ j \ C i = C j" huffman@18071: huffman@18071: finite_chain :: "(nat \ 'a::po) \ bool" huffman@18071: "finite_chain C \ chain(C) \ (\i. max_in_chain i C)" huffman@18071: huffman@18071: lub :: "'a set \ 'a::po" huffman@18071: "lub S \ THE x. S <<| x" nipkow@243: wenzelm@21524: abbreviation wenzelm@21524: Lub (binder "LUB " 10) where wenzelm@21524: "LUB n. t n == lub (range t)" oheimb@2394: wenzelm@21524: notation (xsymbols) wenzelm@21524: Lub (binder "\ " 10) nipkow@243: huffman@15562: huffman@15576: text {* lubs are unique *} huffman@15562: huffman@17810: lemma unique_lub: "\S <<| x; S <<| y\ \ x = y" huffman@15562: apply (unfold is_lub_def is_ub_def) huffman@15562: apply (blast intro: antisym_less) huffman@15562: done huffman@15562: huffman@15576: text {* chains are monotone functions *} huffman@15562: huffman@17810: lemma chain_mono [rule_format]: "chain F \ x < y \ F x \ F y" huffman@15562: apply (unfold chain_def) huffman@17810: apply (induct_tac y) huffman@17810: apply simp huffman@17810: apply (blast elim: less_SucE intro: trans_less) huffman@15562: done huffman@15562: huffman@17810: lemma chain_mono3: "\chain F; x \ y\ \ F x \ F y" huffman@15562: apply (drule le_imp_less_or_eq) huffman@15562: apply (blast intro: chain_mono) huffman@15562: done huffman@15562: huffman@15576: text {* The range of a chain is a totally ordered *} huffman@15562: huffman@17810: lemma chain_tord: "chain F \ tord (range F)" huffman@17810: apply (unfold tord_def, clarify) huffman@15562: apply (rule nat_less_cases) huffman@15562: apply (fast intro: chain_mono)+ huffman@15562: done huffman@15562: huffman@15576: text {* technical lemmas about @{term lub} and @{term is_lub} *} huffman@15562: huffman@15562: lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] huffman@15562: huffman@17810: lemma lubI: "M <<| x \ M <<| lub M" huffman@15930: apply (unfold lub_def) huffman@17810: apply (rule theI) huffman@15930: apply assumption huffman@17810: apply (erule (1) unique_lub) huffman@15562: done huffman@15562: huffman@17810: lemma thelubI: "M <<| l \ lub M = l" huffman@18088: by (rule unique_lub [OF lubI]) huffman@15562: huffman@17810: lemma lub_singleton [simp]: "lub {x} = x" huffman@17810: by (simp add: thelubI is_lub_def is_ub_def) huffman@15562: huffman@15576: text {* access to some definition as inference rule *} huffman@15562: huffman@17810: lemma is_lubD1: "S <<| x \ S <| x" huffman@17810: by (unfold is_lub_def, simp) huffman@15562: huffman@17810: lemma is_lub_lub: "\S <<| x; S <| u\ \ x \ u" huffman@17810: by (unfold is_lub_def, simp) huffman@15562: huffman@17810: lemma is_lubI: "\S <| x; \u. S <| u \ x \ u\ \ S <<| x" huffman@17810: by (unfold is_lub_def, fast) nipkow@243: huffman@17810: lemma chainE: "chain F \ F i \ F (Suc i)" huffman@17810: by (unfold chain_def, simp) huffman@15562: huffman@17810: lemma chainI: "(\i. F i \ F (Suc i)) \ chain F" huffman@17810: by (unfold chain_def, simp) huffman@15562: huffman@17810: lemma chain_shift: "chain Y \ chain (\i. Y (i + j))" huffman@15562: apply (rule chainI) huffman@16318: apply simp huffman@15562: apply (erule chainE) huffman@15562: done huffman@15562: huffman@15576: text {* technical lemmas about (least) upper bounds of chains *} huffman@15562: huffman@17810: lemma ub_rangeD: "range S <| x \ S i \ x" huffman@17810: by (unfold is_ub_def, simp) huffman@15562: huffman@17810: lemma ub_rangeI: "(\i. S i \ x) \ range S <| x" huffman@17810: by (unfold is_ub_def, fast) huffman@15562: huffman@17810: lemma is_ub_lub: "range S <<| x \ S i \ x" huffman@17810: by (rule is_lubD1 [THEN ub_rangeD]) huffman@15562: huffman@16318: lemma is_ub_range_shift: huffman@16318: "chain S \ range (\i. S (i + j)) <| x = range S <| x" huffman@16318: apply (rule iffI) huffman@16318: apply (rule ub_rangeI) huffman@16318: apply (rule_tac y="S (i + j)" in trans_less) huffman@16318: apply (erule chain_mono3) huffman@16318: apply (rule le_add1) huffman@16318: apply (erule ub_rangeD) huffman@16318: apply (rule ub_rangeI) huffman@16318: apply (erule ub_rangeD) huffman@16318: done huffman@16318: huffman@16318: lemma is_lub_range_shift: huffman@16318: "chain S \ range (\i. S (i + j)) <<| x = range S <<| x" huffman@16318: by (simp add: is_lub_def is_ub_range_shift) huffman@16318: huffman@15576: text {* results about finite chains *} huffman@15562: huffman@17810: lemma lub_finch1: "\chain C; max_in_chain i C\ \ range C <<| C i" huffman@15562: apply (unfold max_in_chain_def) huffman@15562: apply (rule is_lubI) huffman@17810: apply (rule ub_rangeI, rename_tac j) huffman@17810: apply (rule_tac x=i and y=j in linorder_le_cases) huffman@17810: apply simp huffman@17810: apply (erule (1) chain_mono3) huffman@15562: apply (erule ub_rangeD) huffman@15562: done huffman@15562: huffman@15562: lemma lub_finch2: huffman@17810: "finite_chain C \ range C <<| C (LEAST i. max_in_chain i C)" huffman@15562: apply (unfold finite_chain_def) huffman@17810: apply (erule conjE) huffman@17810: apply (erule LeastI2_ex) huffman@17810: apply (erule (1) lub_finch1) huffman@15562: done huffman@15562: huffman@19621: lemma finch_imp_finite_range: "finite_chain Y \ finite (range Y)" huffman@19621: apply (unfold finite_chain_def, clarify) huffman@19621: apply (rule_tac f="Y" and n="Suc i" in nat_seg_image_imp_finite) huffman@19621: apply (rule equalityI) huffman@19621: apply (rule subsetI) huffman@19621: apply (erule rangeE, rename_tac j) huffman@19621: apply (rule_tac x=i and y=j in linorder_le_cases) huffman@19621: apply (subgoal_tac "Y j = Y i", simp) huffman@19621: apply (simp add: max_in_chain_def) huffman@19621: apply simp huffman@19621: apply fast huffman@19621: done huffman@19621: huffman@19621: lemma finite_tord_has_max [rule_format]: huffman@19621: "finite S \ S \ {} \ tord S \ (\y\S. \x\S. x \ y)" huffman@19621: apply (erule finite_induct, simp) huffman@19621: apply (rename_tac a S, clarify) huffman@19621: apply (case_tac "S = {}", simp) huffman@19621: apply (drule (1) mp) huffman@19621: apply (drule mp, simp add: tord_def) huffman@19621: apply (erule bexE, rename_tac z) huffman@19621: apply (subgoal_tac "a \ z \ z \ a") huffman@19621: apply (erule disjE) huffman@19621: apply (rule_tac x="z" in bexI, simp, simp) huffman@19621: apply (rule_tac x="a" in bexI) huffman@19621: apply (clarsimp elim!: rev_trans_less) huffman@19621: apply simp huffman@19621: apply (simp add: tord_def) huffman@19621: done huffman@19621: huffman@19621: lemma finite_range_imp_finch: huffman@19621: "\chain Y; finite (range Y)\ \ finite_chain Y" huffman@19621: apply (subgoal_tac "\y\range Y. \x\range Y. x \ y") huffman@19621: apply (clarsimp, rename_tac i) huffman@19621: apply (subgoal_tac "max_in_chain i Y") huffman@19621: apply (simp add: finite_chain_def exI) huffman@19621: apply (simp add: max_in_chain_def po_eq_conv chain_mono3) huffman@19621: apply (erule finite_tord_has_max, simp) huffman@19621: apply (erule chain_tord) huffman@19621: done huffman@19621: huffman@17810: lemma bin_chain: "x \ y \ chain (\i. if i=0 then x else y)" huffman@17810: by (rule chainI, simp) huffman@17810: huffman@17810: lemma bin_chainmax: huffman@17810: "x \ y \ max_in_chain (Suc 0) (\i. if i=0 then x else y)" huffman@17810: by (unfold max_in_chain_def, simp) huffman@15562: huffman@17810: lemma lub_bin_chain: huffman@17810: "x \ y \ range (\i::nat. if i=0 then x else y) <<| y" huffman@17810: apply (frule bin_chain) huffman@17810: apply (drule bin_chainmax) huffman@17810: apply (drule (1) lub_finch1) huffman@17810: apply simp huffman@15562: done huffman@15562: huffman@15576: text {* the maximal element in a chain is its lub *} huffman@15562: huffman@17810: lemma lub_chain_maxelem: "\Y i = c; \i. Y i \ c\ \ lub (range Y) = c" huffman@17810: by (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) huffman@15562: huffman@15576: text {* the lub of a constant chain is the constant *} huffman@15562: huffman@18071: lemma chain_const [simp]: "chain (\i. c)" huffman@17372: by (simp add: chainI) huffman@17372: huffman@17810: lemma lub_const: "range (\x. c) <<| c" huffman@17810: by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) regensbu@1274: huffman@18071: lemma thelub_const [simp]: "(\i. c) = c" huffman@18071: by (rule lub_const [THEN thelubI]) regensbu@1168: huffman@18071: end