src/HOLCF/Porder.thy
 changeset 1479 21eb5e156d91 parent 1274 ea0668a1c0ba child 2278 d63ffafce255
equal inserted replaced
1478:2b8c2a7547ab 1479:21eb5e156d91
`     1 (*  Title: 	HOLCF/porder.thy`
`     1 (*  Title:      HOLCF/porder.thy`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author: 	Franz Regensburger`
`     3     Author:     Franz Regensburger`
`     4     Copyright   1993 Technische Universitaet Muenchen`
`     4     Copyright   1993 Technische Universitaet Muenchen`
`     5 `
`     5 `
`     6 Conservative extension of theory Porder0 by constant definitions `
`     6 Conservative extension of theory Porder0 by constant definitions `
`     7 `
`     7 `
`     8 *)`
`     8 *)`
`     9 `
`     9 `
`    10 Porder = Porder0 +`
`    10 Porder = Porder0 +`
`    11 `
`    11 `
`    12 consts	`
`    12 consts  `
`    13 	"<|"	::	"['a set,'a::po] => bool"	(infixl 55)`
`    13         "<|"    ::      "['a set,'a::po] => bool"       (infixl 55)`
`    14 	"<<|"	::	"['a set,'a::po] => bool"	(infixl 55)`
`    14         "<<|"   ::      "['a set,'a::po] => bool"       (infixl 55)`
`    15 	lub	::	"'a set => 'a::po"`
`    15         lub     ::      "'a set => 'a::po"`
`    16 	is_tord	::	"'a::po set => bool"`
`    16         is_tord ::      "'a::po set => bool"`
`    17 	is_chain ::	"(nat=>'a::po) => bool"`
`    17         is_chain ::     "(nat=>'a::po) => bool"`
`    18 	max_in_chain :: "[nat,nat=>'a::po]=>bool"`
`    18         max_in_chain :: "[nat,nat=>'a::po]=>bool"`
`    19 	finite_chain :: "(nat=>'a::po)=>bool"`
`    19         finite_chain :: "(nat=>'a::po)=>bool"`
`    20 `
`    20 `
`    21 defs`
`    21 defs`
`    22 `
`    22 `
`    23 (* class definitions *)`
`    23 (* class definitions *)`
`    24 `
`    24 `
`    25 is_ub		"S  <| x == ! y.y:S --> y<<x"`
`    25 is_ub           "S  <| x == ! y.y:S --> y<<x"`
`    26 is_lub		"S <<| x == S <| x & (! u. S <| u  --> x << u)"`
`    26 is_lub          "S <<| x == S <| x & (! u. S <| u  --> x << u)"`
`    27 `
`    27 `
`    28 `
`    28 `
`    29 (* Arbitrary chains are total orders    *)                  `
`    29 (* Arbitrary chains are total orders    *)                  `
`    30 is_tord		"is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"`
`    30 is_tord         "is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"`
`    31 `
`    31 `
`    32 (* Here we use countable chains and I prefer to code them as functions! *)`
`    32 (* Here we use countable chains and I prefer to code them as functions! *)`
`    33 is_chain	"is_chain(F) == (! i.F(i) << F(Suc(i)))"`
`    33 is_chain        "is_chain(F) == (! i.F(i) << F(Suc(i)))"`
`    34 `
`    34 `
`    35 (* finite chains, needed for monotony of continouous functions *)`
`    35 (* finite chains, needed for monotony of continouous functions *)`
`    36 `
`    36 `
`    37 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" `
`    37 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" `
`    38 `
`    38 `
`    39 finite_chain_def "finite_chain(C) == is_chain(C) & (? i. max_in_chain i C)"`
`    39 finite_chain_def "finite_chain(C) == is_chain(C) & (? i. max_in_chain i C)"`
`    40 `
`    40 `
`    41 rules`
`    41 rules`
`    42 `
`    42 `
`    43 lub		"lub(S) = (@x. S <<| x)"`
`    43 lub             "lub(S) = (@x. S <<| x)"`
`    44 `
`    44 `
`    45 (* start 8bit 1 *)`
`    45 (* start 8bit 1 *)`
`    46 (* end 8bit 1 *)`
`    46 (* end 8bit 1 *)`
`    47 `
`    47 `
`    48 end `
`    48 end `