summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Sequents/LK0.ML

author | paulson |

Wed Jul 28 13:55:02 1999 +0200 (1999-07-28) | |

changeset 7122 | 87b233b31889 |

parent 7093 | b2ee0e5d1a7f |

child 9259 | 103acc345f75 |

permissions | -rw-r--r-- |

renamed ...thm_pack... to ...pack...

1 (* Title: LK/LK0

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1992 University of Cambridge

6 Tactics and lemmas for LK (thanks also to Philippe de Groote)

8 Structural rules by Soren Heilmann

9 *)

11 (** Structural Rules on formulas **)

13 (*contraction*)

15 Goal "$H |- $E, P, P, $F ==> $H |- $E, P, $F";

16 by (etac contRS 1);

17 qed "contR";

19 Goal "$H, P, P, $G |- $E ==> $H, P, $G |- $E";

20 by (etac contLS 1);

21 qed "contL";

23 (*thinning*)

25 Goal "$H |- $E, $F ==> $H |- $E, P, $F";

26 by (etac thinRS 1);

27 qed "thinR";

29 Goal "$H, $G |- $E ==> $H, P, $G |- $E";

30 by (etac thinLS 1);

31 qed "thinL";

33 (*exchange*)

35 Goal "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F";

36 by (etac exchRS 1);

37 qed "exchR";

39 Goal "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E";

40 by (etac exchLS 1);

41 qed "exchL";

43 (*Cut and thin, replacing the right-side formula*)

44 fun cutR_tac (sP: string) i =

45 res_inst_tac [ ("P",sP) ] cut i THEN rtac thinR i;

47 (*Cut and thin, replacing the left-side formula*)

48 fun cutL_tac (sP: string) i =

49 res_inst_tac [ ("P",sP) ] cut i THEN rtac thinL (i+1);

52 (** If-and-only-if rules **)

53 Goalw [iff_def]

54 "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F";

55 by (REPEAT (ares_tac [conjR,impR] 1));

56 qed "iffR";

58 Goalw [iff_def]

59 "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E";

60 by (REPEAT (ares_tac [conjL,impL,basic] 1));

61 qed "iffL";

63 Goal "$H |- $E, (P <-> P), $F";

64 by (REPEAT (resolve_tac [iffR,basic] 1));

65 qed "iff_refl";

67 Goalw [True_def] "$H |- $E, True, $F";

68 by (rtac impR 1);

69 by (rtac basic 1);

70 qed "TrueR";

72 (*Descriptions*)

73 val [p1,p2] = Goal

74 "[| $H |- $E, P(a), $F; !!x. $H, P(x) |- $E, x=a, $F |] \

75 \ ==> $H |- $E, (THE x. P(x)) = a, $F";

76 by (rtac cut 1);

77 by (rtac p2 2);

78 by (rtac The 1 THEN rtac thinR 1 THEN rtac exchRS 1 THEN rtac p1 1);

79 by (rtac thinR 1 THEN rtac exchRS 1 THEN rtac p2 1);

80 qed "the_equality";

82 (** Weakened quantifier rules. Incomplete, they let the search terminate.**)

84 Goal "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E";

85 by (rtac allL 1);

86 by (etac thinL 1);

87 qed "allL_thin";

89 Goal "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F";

90 by (rtac exR 1);

91 by (etac thinR 1);

92 qed "exR_thin";

95 (*The rules of LK*)

96 val prop_pack = empty_pack add_safes

97 [basic, refl, TrueR, FalseL,

98 conjL, conjR, disjL, disjR, impL, impR,

99 notL, notR, iffL, iffR];

101 val LK_pack = prop_pack add_safes [allR, exL]

102 add_unsafes [allL_thin, exR_thin, the_equality];

104 val LK_dup_pack = prop_pack add_safes [allR, exL]

105 add_unsafes [allL, exR, the_equality];

108 pack_ref() := LK_pack;

110 fun lemma_tac th i =

111 rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;

113 val [major,minor] = goal thy

114 "[| $H |- $E, $F, P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F";

115 by (rtac (thinRS RS cut) 1 THEN rtac major 1);

116 by (Step_tac 1);

117 by (rtac thinR 1 THEN rtac minor 1);

118 qed "mp_R";

120 val [major,minor] = goal thy

121 "[| $H, $G |- $E, P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E";

122 by (rtac (thinL RS cut) 1 THEN rtac major 1);

123 by (Step_tac 1);

124 by (rtac thinL 1 THEN rtac minor 1);

125 qed "mp_L";

128 (** Two rules to generate left- and right- rules from implications **)

130 val [major,minor] = goal thy

131 "[| |- P --> Q; $H |- $E, $F, P |] ==> $H |- $E, Q, $F";

132 by (rtac mp_R 1);

133 by (rtac minor 2);

134 by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);

135 qed "R_of_imp";

137 val [major,minor] = goal thy

138 "[| |- P --> Q; $H, $G, Q |- $E |] ==> $H, P, $G |- $E";

139 by (rtac mp_L 1);

140 by (rtac minor 2);

141 by (rtac thinRS 1 THEN rtac (major RS thinLS) 1);

142 qed "L_of_imp";

144 (*Can be used to create implications in a subgoal*)

145 val [prem] = goal thy

146 "[| $H, $G |- $E, $F, P --> Q |] ==> $H, P, $G |- $E, Q, $F";

147 by (rtac mp_L 1);

148 by (rtac basic 2);

149 by (rtac thinR 1 THEN rtac prem 1);

150 qed "backwards_impR";

153 qed_goal "conjunct1" thy "|-P&Q ==> |-P"

154 (fn [major] => [lemma_tac major 1, Fast_tac 1]);

156 qed_goal "conjunct2" thy "|-P&Q ==> |-Q"

157 (fn [major] => [lemma_tac major 1, Fast_tac 1]);

159 qed_goal "spec" thy "|- (ALL x. P(x)) ==> |- P(x)"

160 (fn [major] => [lemma_tac major 1, Fast_tac 1]);

162 (** Equality **)

164 Goal "|- a=b --> b=a";

165 by (safe_tac (LK_pack add_safes [subst]) 1);

166 qed "sym";

168 Goal "|- a=b --> b=c --> a=c";

169 by (safe_tac (LK_pack add_safes [subst]) 1);

170 qed "trans";

172 (* Symmetry of equality in hypotheses *)

173 bind_thm ("symL", sym RS L_of_imp);

175 (* Symmetry of equality in hypotheses *)

176 bind_thm ("symR", sym RS R_of_imp);

178 Goal "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F";

179 by (rtac (trans RS R_of_imp RS mp_R) 1);

180 by (ALLGOALS assume_tac);

181 qed "transR";

184 (* Two theorms for rewriting only one instance of a definition:

185 the first for definitions of formulae and the second for terms *)

187 val prems = goal thy "(A == B) ==> |- A <-> B";

188 by (rewrite_goals_tac prems);

189 by (rtac iff_refl 1);

190 qed "def_imp_iff";

192 val prems = goal thy "(A == B) ==> |- A = B";

193 by (rewrite_goals_tac prems);

194 by (rtac refl 1);

195 qed "meta_eq_to_obj_eq";