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

src/HOL/meson_lemmas.ML

author | oheimb |

Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) | |

changeset 11008 | f7333f055ef6 |

parent 9970 | dfe4747c8318 |

child 11460 | e5fb885bfe3a |

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

improved theory reference in comment

1 (* Title: HOL/meson_lemmas.ML

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1992 University of Cambridge

6 Lemmas for Meson.

7 *)

9 (* "Axiom" of Choice, proved using the description operator *)

11 Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";

12 by (fast_tac (claset() addEs [someI]) 1);

13 qed "choice";

16 (* Generation of contrapositives *)

18 (*Inserts negated disjunct after removing the negation; P is a literal*)

19 val [major,minor] = Goal "~P|Q ==> ((~P==>P) ==> Q)";

20 by (rtac (major RS disjE) 1);

21 by (rtac notE 1);

22 by (etac minor 2);

23 by (ALLGOALS assume_tac);

24 qed "make_neg_rule";

26 (*For Plaisted's "Postive refinement" of the MESON procedure*)

27 Goal "~P|Q ==> (P ==> Q)";

28 by (Blast_tac 1);

29 qed "make_refined_neg_rule";

31 (*P should be a literal*)

32 val [major,minor] = Goal "P|Q ==> ((P==>~P) ==> Q)";

33 by (rtac (major RS disjE) 1);

34 by (rtac notE 1);

35 by (etac minor 1);

36 by (ALLGOALS assume_tac);

37 qed "make_pos_rule";

40 (* Generation of a goal clause -- put away the final literal *)

42 val [major,minor] = Goal "~P ==> ((~P==>P) ==> False)";

43 by (rtac notE 1);

44 by (rtac minor 2);

45 by (ALLGOALS (rtac major));

46 qed "make_neg_goal";

48 val [major,minor] = Goal "P ==> ((P==>~P) ==> False)";

49 by (rtac notE 1);

50 by (rtac minor 1);

51 by (ALLGOALS (rtac major));

52 qed "make_pos_goal";

55 (* Lemmas for forward proof (like congruence rules) *)

57 (*NOTE: could handle conjunctions (faster?) by

58 nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *)

59 val major::prems = Goal

60 "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q";

61 by (rtac (major RS conjE) 1);

62 by (rtac conjI 1);

63 by (ALLGOALS (eresolve_tac prems));

64 qed "conj_forward";

66 val major::prems = Goal

67 "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q";

68 by (rtac (major RS disjE) 1);

69 by (ALLGOALS (dresolve_tac prems));

70 by (ALLGOALS (eresolve_tac [disjI1,disjI2]));

71 qed "disj_forward";

73 (*Version for removal of duplicate literals*)

74 val major::prems = Goal

75 "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q";

76 by (cut_facts_tac [major] 1);

77 by (blast_tac (claset() addIs prems) 1);

78 qed "disj_forward2";

80 val major::prems = Goal

81 "[| ALL x. P'(x); !!x. P'(x) ==> P(x) |] ==> ALL x. P(x)";

82 by (rtac allI 1);

83 by (resolve_tac prems 1);

84 by (rtac (major RS spec) 1);

85 qed "all_forward";

87 val major::prems = Goal

88 "[| EX x. P'(x); !!x. P'(x) ==> P(x) |] ==> EX x. P(x)";

89 by (rtac (major RS exE) 1);

90 by (rtac exI 1);

91 by (eresolve_tac prems 1);

92 qed "ex_forward";