src/HOLCF/Porder.thy
 changeset 15587 f363e6e080e7 parent 15577 e16da3068ad6 child 15600 a59f07556a8d
equal inserted replaced
15586:f7f812034707 15587:f363e6e080e7
`     5 `
`     5 `
`     6 Definition of class porder (partial order).`
`     6 Definition of class porder (partial order).`
`     7 Conservative extension of theory Porder0 by constant definitions `
`     7 Conservative extension of theory Porder0 by constant definitions `
`     8 *)`
`     8 *)`
`     9 `
`     9 `
`    10 header {* Type class of partial orders *}`
`    10 header {* Partial orders *}`
`    11 `
`    11 `
`    12 theory Porder`
`    12 theory Porder`
`    13 imports Main`
`    13 imports Main`
`    14 begin`
`    14 begin`
`    15 `
`    15 `
`    16 	(* introduce a (syntactic) class for the constant << *)`
`    16 subsection {* Type class for partial orders *}`
`       `
`    17 `
`       `
`    18 	-- {* introduce a (syntactic) class for the constant @{text "<<"} *}`
`    17 axclass sq_ord < type`
`    19 axclass sq_ord < type`
`    18 `
`    20 `
`    19 	(* characteristic constant << for po *)`
`    21 	-- {* characteristic constant @{text "<<"} for po *}`
`    20 consts`
`    22 consts`
`    21   "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)`
`    23   "<<"          :: "['a,'a::sq_ord] => bool"        (infixl 55)`
`    22 `
`    24 `
`    23 syntax (xsymbols)`
`    25 syntax (xsymbols)`
`    24   "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\<sqsubseteq>" 55)`
`    26   "op <<"       :: "['a,'a::sq_ord] => bool"        (infixl "\<sqsubseteq>" 55)`
`    25 `
`    27 `
`    26 axclass po < sq_ord`
`    28 axclass po < sq_ord`
`    27         (* class axioms: *)`
`    29         -- {* class axioms: *}`
`    28 refl_less [iff]: "x << x"        `
`    30 refl_less [iff]: "x << x"        `
`    29 antisym_less:    "[|x << y; y << x |] ==> x = y"    `
`    31 antisym_less:    "[|x << y; y << x |] ==> x = y"    `
`    30 trans_less:      "[|x << y; y << z |] ==> x << z"`
`    32 trans_less:      "[|x << y; y << z |] ==> x << z"`
`    31 `
`    33 `
`    32 text {* minimal fixes least element *}`
`    34 text {* minimal fixes least element *}`
`    49 `
`    51 `
`    50 lemma po_eq_conv: "((x::'a::po)=y) = (x << y & y << x)"`
`    52 lemma po_eq_conv: "((x::'a::po)=y) = (x << y & y << x)"`
`    51 apply (fast elim!: antisym_less_inverse intro!: antisym_less)`
`    53 apply (fast elim!: antisym_less_inverse intro!: antisym_less)`
`    52 done`
`    54 done`
`    53 `
`    55 `
`    54 subsection {* Constant definitions *}`
`    56 subsection {* Chains and least upper bounds *}`
`    55 `
`    57 `
`    56 consts  `
`    58 consts  `
`    57         "<|"    ::      "['a set,'a::po] => bool"       (infixl 55)`
`    59         "<|"    ::      "['a set,'a::po] => bool"       (infixl 55)`
`    58         "<<|"   ::      "['a set,'a::po] => bool"       (infixl 55)`
`    60         "<<|"   ::      "['a set,'a::po] => bool"       (infixl 55)`
`    59         lub     ::      "'a set => 'a::po"`
`    61         lub     ::      "'a set => 'a::po"`
`    71 syntax (xsymbols)`
`    73 syntax (xsymbols)`
`    72   "LUB "	:: "[idts, 'a] => 'a"		("(3\<Squnion>_./ _)"[0,10] 10)`
`    74   "LUB "	:: "[idts, 'a] => 'a"		("(3\<Squnion>_./ _)"[0,10] 10)`
`    73 `
`    75 `
`    74 defs`
`    76 defs`
`    75 `
`    77 `
`    76 (* class definitions *)`
`    78 -- {* class definitions *}`
`    77 is_ub_def:       "S  <| x == ! y. y:S --> y<<x"`
`    79 is_ub_def:       "S  <| x == ! y. y:S --> y<<x"`
`    78 is_lub_def:      "S <<| x == S <| x & (!u. S <| u  --> x << u)"`
`    80 is_lub_def:      "S <<| x == S <| x & (!u. S <| u  --> x << u)"`
`    79 `
`    81 `
`    80 (* Arbitrary chains are total orders    *)                  `
`    82 -- {* Arbitrary chains are total orders *}`
`    81 tord_def:     "tord S == !x y. x:S & y:S --> (x<<y | y<<x)"`
`    83 tord_def:     "tord S == !x y. x:S & y:S --> (x<<y | y<<x)"`
`    82 `
`    84 `
`    83 (* Here we use countable chains and I prefer to code them as functions! *)`
`    85 -- {* Here we use countable chains and I prefer to code them as functions! *}`
`    84 chain_def:        "chain F == !i. F i << F (Suc i)"`
`    86 chain_def:        "chain F == !i. F i << F (Suc i)"`
`    85 `
`    87 `
`    86 (* finite chains, needed for monotony of continouous functions *)`
`    88 -- {* finite chains, needed for monotony of continouous functions *}`
`    87 max_in_chain_def: "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" `
`    89 max_in_chain_def: "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" `
`    88 finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)"`
`    90 finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)"`
`    89 `
`    91 `
`    90 lub_def:          "lub S == (@x. S <<| x)"`
`    92 lub_def:          "lub S == (@x. S <<| x)"`
`    91 `
`    93 `
`   185 apply (unfold is_ub_def)`
`   187 apply (unfold is_ub_def)`
`   186 apply blast`
`   188 apply blast`
`   187 done`
`   189 done`
`   188 `
`   190 `
`   189 lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard]`
`   191 lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard]`
`   190 (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1                                    *)`
`   192   -- {* @{thm is_ub_lub} *} (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)`
`   191 `
`   193 `
`   192 text {* results about finite chains *}`
`   194 text {* results about finite chains *}`
`   193 `
`   195 `
`   194 lemma lub_finch1: `
`   196 lemma lub_finch1: `
`   195         "[| chain C; max_in_chain i C|] ==> range C <<| C i"`
`   197         "[| chain C; max_in_chain i C|] ==> range C <<| C i"`