src/HOLCF/Porder.thy
changeset 15587 f363e6e080e7
parent 15577 e16da3068ad6
child 15600 a59f07556a8d
equal deleted 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"