author  huffman 
Sun, 28 Feb 2010 14:55:42 0800  
changeset 35473  c4d3d65856dd 
parent 33588  ea9becc59636 
child 35906  e0382e4b4da7 
permissions  rwrr 
1479  1 
(* Title: HOLCF/HOLCF.thy 
2 
Author: Franz Regensburger 

243
c22b85994e17
Franz Regensburger's HigherOrder 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 HigherOrder Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset

5 
*) 
c22b85994e17
Franz Regensburger's HigherOrder 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 

12 
Sum_Cpo 

16841  13 
uses 
14 
"holcf_logic.ML" 

23152  15 
"Tools/adm_tac.ML" 
15650  16 
begin 
17 

25904  18 
defaultsort pcpo 
19 

26339  20 
declaration {* fn _ => 
21 
Simplifier.map_ss (fn simpset => simpset addSolver 

17612  22 
(mk_solver' "adm_tac" (fn ss => 
30603  23 
Adm.adm_tac (Simplifier.the_context ss) 
24 
(cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss)))); 

16841  25 
*} 
26 

31076
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

27 
text {* Legacy theorem names *} 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

28 

99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

29 
lemmas sq_ord_less_eq_trans = below_eq_trans 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

30 
lemmas sq_ord_eq_less_trans = eq_below_trans 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

31 
lemmas refl_less = below_refl 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

32 
lemmas trans_less = below_trans 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

33 
lemmas antisym_less = below_antisym 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

34 
lemmas antisym_less_inverse = below_antisym_inverse 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

35 
lemmas box_less = box_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

36 
lemmas rev_trans_less = rev_below_trans 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

37 
lemmas not_less2not_eq = not_below2not_eq 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

38 
lemmas less_UU_iff = below_UU_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

39 
lemmas flat_less_iff = flat_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

40 
lemmas adm_less = adm_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

41 
lemmas adm_not_less = adm_not_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

42 
lemmas adm_compact_not_less = adm_compact_not_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

43 
lemmas less_fun_def = below_fun_def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

44 
lemmas expand_fun_less = expand_fun_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

45 
lemmas less_fun_ext = below_fun_ext 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

46 
lemmas less_discr_def = below_discr_def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

47 
lemmas discr_less_eq = discr_below_eq 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

48 
lemmas less_unit_def = below_unit_def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

49 
lemmas less_cprod_def = below_prod_def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

50 
lemmas prod_lessI = prod_belowI 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

51 
lemmas Pair_less_iff = Pair_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

52 
lemmas fst_less_iff = fst_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

53 
lemmas snd_less_iff = snd_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

54 
lemmas expand_cfun_less = expand_cfun_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

55 
lemmas less_cfun_ext = below_cfun_ext 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

56 
lemmas injection_less = injection_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

57 
lemmas approx_less = approx_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

58 
lemmas profinite_less_ext = profinite_below_ext 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

59 
lemmas less_up_def = below_up_def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

60 
lemmas not_Iup_less = not_Iup_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

61 
lemmas Iup_less = Iup_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

62 
lemmas up_less = up_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

63 
lemmas cpair_less = cpair_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

64 
lemmas less_cprod = below_cprod 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

65 
lemmas cfst_less_iff = cfst_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

66 
lemmas csnd_less_iff = csnd_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

67 
lemmas Def_inject_less_eq = Def_below_Def 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

68 
lemmas Def_less_is_eq = Def_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

69 
lemmas spair_less_iff = spair_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

70 
lemmas less_sprod = below_sprod 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

71 
lemmas spair_less = spair_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

72 
lemmas sfst_less_iff = sfst_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

73 
lemmas ssnd_less_iff = ssnd_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

74 
lemmas fix_least_less = fix_least_below 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

75 
lemmas dist_less_one = dist_below_one 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

76 
lemmas less_ONE = below_ONE 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

77 
lemmas ONE_less_iff = ONE_below_iff 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

78 
lemmas less_sinlD = below_sinlD 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

79 
lemmas less_sinrD = below_sinrD 
99fe356cbbc2
rename constant sq_le to below; rename class sq_ord to below; less>below in many lemma names
huffman
parents:
30910
diff
changeset

80 

15650  81 
end 