author | wenzelm |
Tue, 29 Mar 2011 17:47:11 +0200 | |
changeset 42151 | 4da4fc77664b |
parent 41886 | aa8dce9ab8a9 |
child 45049 | 13efaee97111 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/HOLCF.thy |
1479 | 2 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
3 |
|
16841 | 4 |
HOLCF -- a semantic extension of HOL by the LCF logic. |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
|
15650 | 7 |
theory HOLCF |
29130 | 8 |
imports |
35473 | 9 |
Main |
10 |
Domain |
|
11 |
Powerdomains |
|
15650 | 12 |
begin |
13 |
||
40497 | 14 |
default_sort "domain" |
25904 | 15 |
|
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
16 |
text {* Legacy theorem names deprecated after Isabelle2009-2: *} |
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
17 |
|
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
18 |
lemmas expand_fun_below = fun_below_iff |
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
19 |
lemmas below_fun_ext = fun_belowI |
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
20 |
lemmas expand_cfun_eq = cfun_eq_iff |
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
21 |
lemmas ext_cfun = cfun_eqI |
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
22 |
lemmas expand_cfun_below = cfun_below_iff |
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
23 |
lemmas below_cfun_ext = cfun_belowI |
40011
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40002
diff
changeset
|
24 |
lemmas monofun_fun_fun = fun_belowD |
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40002
diff
changeset
|
25 |
lemmas monofun_fun_arg = monofunE |
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40002
diff
changeset
|
26 |
lemmas monofun_lub_fun = adm_monofun [THEN admD] |
b974cf829099
cleaned up Fun_Cpo.thy; deprecated a few theorem names
huffman
parents:
40002
diff
changeset
|
27 |
lemmas cont_lub_fun = adm_cont [THEN admD] |
40326
73d45866dbda
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
huffman
parents:
40011
diff
changeset
|
28 |
lemmas cont2cont_Rep_CFun = cont2cont_APP |
73d45866dbda
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
huffman
parents:
40011
diff
changeset
|
29 |
lemmas cont_Rep_CFun_app = cont_APP_app |
73d45866dbda
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
huffman
parents:
40011
diff
changeset
|
30 |
lemmas cont_Rep_CFun_app_app = cont_APP_app_app |
40771 | 31 |
lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE] |
32 |
lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE] |
|
41027 | 33 |
lemmas contlub_cfun = lub_APP [symmetric] |
34 |
lemmas contlub_LAM = lub_LAM [symmetric] |
|
40771 | 35 |
lemmas thelubI = lub_eqI |
41430
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41414
diff
changeset
|
36 |
lemmas UU_I = bottomI |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41414
diff
changeset
|
37 |
lemmas lift_distinct1 = lift.distinct(1) |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41414
diff
changeset
|
38 |
lemmas lift_distinct2 = lift.distinct(2) |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41414
diff
changeset
|
39 |
lemmas Def_not_UU = lift.distinct(2) |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41414
diff
changeset
|
40 |
lemmas Def_inject = lift.inject |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41414
diff
changeset
|
41 |
lemmas below_UU_iff = below_bottom_iff |
1aa23e9f2c87
change some lemma names containing 'UU' to 'bottom'
huffman
parents:
41414
diff
changeset
|
42 |
lemmas eq_UU_iff = eq_bottom_iff |
40002
c5b5f7a3a3b1
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
huffman
parents:
39974
diff
changeset
|
43 |
|
15650 | 44 |
end |