author  clasohm 
Wed, 29 Jun 1994 12:03:41 +0200  
changeset 442  13ac1fd0a14d 
parent 0  a5a9c433f639 
child 1461  6bcb44e4d6e5 
permissions  rwrr 
0  1 
(* Title: LCF/lcf.ML 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow 

4 
Copyright 1992 University of Cambridge 

5 

6 
For lcf.thy. Basic lemmas about LCF 

7 
*) 

8 

9 
open LCF; 

10 

11 
signature LCF_LEMMAS = 

12 
sig 

13 
val ap_term: thm 

14 
val ap_thm: thm 

15 
val COND_cases: thm 

16 
val COND_cases_iff: thm 

17 
val Contrapos: thm 

18 
val cong: thm 

19 
val ext: thm 

20 
val eq_imp_less1: thm 

21 
val eq_imp_less2: thm 

22 
val less_anti_sym: thm 

23 
val less_ap_term: thm 

24 
val less_ap_thm: thm 

25 
val less_refl: thm 

26 
val less_UU: thm 

27 
val not_UU_eq_TT: thm 

28 
val not_UU_eq_FF: thm 

29 
val not_TT_eq_UU: thm 

30 
val not_TT_eq_FF: thm 

31 
val not_FF_eq_UU: thm 

32 
val not_FF_eq_TT: thm 

33 
val rstac: thm list > int > tactic 

34 
val stac: thm > int > tactic 

35 
val sstac: thm list > int > tactic 

36 
val strip_tac: int > tactic 

37 
val tr_induct: thm 

38 
val UU_abs: thm 

39 
val UU_app: thm 

40 
end; 

41 

42 

43 
structure LCF_Lemmas : LCF_LEMMAS = 

44 

45 
struct 

46 

47 
(* Standard abbreviations *) 

48 

49 
val rstac = resolve_tac; 

50 
fun stac th = rtac(th RS sym RS subst); 

51 
fun sstac ths = EVERY' (map stac ths); 

52 

53 
fun strip_tac i = REPEAT(rstac [impI,allI] i); 

54 

55 
val eq_imp_less1 = prove_goal thy "x=y ==> x << y" 

56 
(fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct1) 1]); 

57 

58 
val eq_imp_less2 = prove_goal thy "x=y ==> y << x" 

59 
(fn prems => [rtac (rewrite_rule[eq_def](hd prems) RS conjunct2) 1]); 

60 

61 
val less_refl = refl RS eq_imp_less1; 

62 

63 
val less_anti_sym = prove_goal thy "[ x << y; y << x ] ==> x=y" 

64 
(fn prems => [rewrite_goals_tac[eq_def], 

65 
REPEAT(rstac(conjI::prems)1)]); 

66 

67 
val ext = prove_goal thy 

442
13ac1fd0a14d
added parentheses made necessary by change of constrain's precedence
clasohm
parents:
0
diff
changeset

68 
"(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))" 
0  69 
(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI, 
70 
prem RS eq_imp_less1, 

71 
prem RS eq_imp_less2]1)]); 

72 

73 
val cong = prove_goal thy "[ f=g; x=y ] ==> f(x)=g(y)" 

74 
(fn prems => [cut_facts_tac prems 1, etac subst 1, etac subst 1, 

75 
rtac refl 1]); 

76 

77 
val less_ap_term = less_refl RS mono; 

78 
val less_ap_thm = less_refl RSN (2,mono); 

79 
val ap_term = refl RS cong; 

80 
val ap_thm = refl RSN (2,cong); 

81 

82 
val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU" 

83 
(fn _ => [rtac less_anti_sym 1, rtac minimal 2, 

84 
rtac less_ext 1, rtac allI 1, rtac minimal 1]); 

85 

86 
val UU_app = UU_abs RS sym RS ap_thm; 

87 

88 
val less_UU = prove_goal thy "x << UU ==> x=UU" 

89 
(fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]); 

90 

91 

92 
val tr_induct = prove_goal thy "[ P(UU); P(TT); P(FF) ] ==> ALL b.P(b)" 

93 
(fn prems => [rtac allI 1, rtac mp 1, 

94 
res_inst_tac[("p","b")]tr_cases 2, 

95 
fast_tac (FOL_cs addIs prems) 1]); 

96 

97 

98 
val Contrapos = prove_goal thy "(A ==> B) ==> (~B ==> ~A)" 

99 
(fn prems => [rtac notI 1, rtac notE 1, rstac prems 1, 

100 
rstac prems 1, atac 1]); 

101 

102 
val not_less_imp_not_eq1 = eq_imp_less1 COMP Contrapos; 

103 
val not_less_imp_not_eq2 = eq_imp_less2 COMP Contrapos; 

104 

105 
val not_UU_eq_TT = not_TT_less_UU RS not_less_imp_not_eq2; 

106 
val not_UU_eq_FF = not_FF_less_UU RS not_less_imp_not_eq2; 

107 
val not_TT_eq_UU = not_TT_less_UU RS not_less_imp_not_eq1; 

108 
val not_TT_eq_FF = not_TT_less_FF RS not_less_imp_not_eq1; 

109 
val not_FF_eq_UU = not_FF_less_UU RS not_less_imp_not_eq1; 

110 
val not_FF_eq_TT = not_FF_less_TT RS not_less_imp_not_eq1; 

111 

112 

113 
val COND_cases_iff = (prove_goal thy 

114 
"ALL b. P(b=>xy) <> (b=UU>P(UU)) & (b=TT>P(x)) & (b=FF>P(y))" 

115 
(fn _ => [cut_facts_tac [not_UU_eq_TT,not_UU_eq_FF,not_TT_eq_UU, 

116 
not_TT_eq_FF,not_FF_eq_UU,not_FF_eq_TT]1, 

117 
rtac tr_induct 1, stac COND_UU 1, stac COND_TT 2, 

118 
stac COND_FF 3, REPEAT(fast_tac FOL_cs 1)])) RS spec; 

119 

120 
val lemma = prove_goal thy "A<>B ==> B ==> A" 

121 
(fn prems => [cut_facts_tac prems 1, rewrite_goals_tac [iff_def], 

122 
fast_tac FOL_cs 1]); 

123 

124 
val COND_cases = conjI RSN (2,conjI RS (COND_cases_iff RS lemma)); 

125 

126 
end; 

127 

128 
open LCF_Lemmas; 

129 