|
1 theory Rules = Main: |
|
2 |
|
3 section{*The Rules of the Game*} |
|
4 |
|
5 |
|
6 subsection{*Introduction Rules*} |
|
7 |
|
8 thm impI conjI disjI1 disjI2 iffI |
|
9 |
|
10 lemma "A \<Longrightarrow> B \<longrightarrow> A \<and> (B \<and> A)" |
|
11 apply(rule impI) |
|
12 apply(rule conjI) |
|
13 apply assumption |
|
14 apply(rule conjI) |
|
15 apply assumption |
|
16 apply assumption |
|
17 done |
|
18 |
|
19 |
|
20 subsection{*Elimination Rules*} |
|
21 |
|
22 thm impE mp |
|
23 thm conjE |
|
24 thm disjE |
|
25 |
|
26 lemma disj_swap: "P | Q \<Longrightarrow> Q | P" |
|
27 apply (erule disjE) |
|
28 apply (rule disjI2) |
|
29 apply assumption |
|
30 apply (rule disjI1) |
|
31 apply assumption |
|
32 done |
|
33 |
|
34 |
|
35 subsection{*Destruction Rules*} |
|
36 |
|
37 thm conjunct1 conjunct1 iffD1 iffD2 |
|
38 lemma conj_swap: "P \<and> Q \<Longrightarrow> Q \<and> P" |
|
39 apply (rule conjI) |
|
40 apply (drule conjunct2) |
|
41 apply assumption |
|
42 apply (drule conjunct1) |
|
43 apply assumption |
|
44 done |
|
45 |
|
46 |
|
47 subsection{*Quantifiers*} |
|
48 |
|
49 |
|
50 thm allI exI |
|
51 thm allE exE |
|
52 thm spec |
|
53 |
|
54 lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y" |
|
55 oops |
|
56 |
|
57 subsection{*Instantiation*} |
|
58 |
|
59 lemma "\<exists>xs. xs @ xs = xs" |
|
60 apply(rule_tac x = "[]" in exI) |
|
61 by simp |
|
62 |
|
63 lemma "\<forall>xs. f(xs @ xs) = xs \<Longrightarrow> f [] = []" |
|
64 apply(erule_tac x = "[]" in allE) |
|
65 by simp |
|
66 |
|
67 |
|
68 subsection{*Hilbert's epsilon Operator*} |
|
69 |
|
70 theorem axiom_of_choice: |
|
71 "\<forall>x. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)" |
|
72 by (fast elim!: someI) |
|
73 |
|
74 |
|
75 subsection{*Automation*} |
|
76 |
|
77 lemma "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and> |
|
78 \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and> |
|
79 (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and> |
|
80 (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and> |
|
81 (\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x)) |
|
82 \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))"; |
|
83 by blast |
|
84 |
|
85 lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) = |
|
86 (\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))" |
|
87 by fast |
|
88 |
|
89 lemma "\<exists>x.\<forall>y. P x y \<Longrightarrow> \<forall>y.\<exists>x. P x y" |
|
90 apply(clarify) |
|
91 by blast |
|
92 |
|
93 |
|
94 subsection{*Forward Proof*} |
|
95 |
|
96 thm rev_rev_ident |
|
97 thm rev_rev_ident[of "[]"] |
|
98 thm sym |
|
99 thm sym[OF rev_rev_ident] |
|
100 thm rev_rev_ident[THEN sym] |
|
101 |
|
102 |
|
103 subsection{*Further Useful Methods*} |
|
104 |
|
105 lemma "n \<le> 1 \<and> n \<noteq> 0 \<Longrightarrow> n^n = n" |
|
106 apply(subgoal_tac "n=1") |
|
107 apply simp |
|
108 apply arith |
|
109 done |
|
110 |
|
111 |
|
112 lemma "\<lbrakk> 2 \<in> Q; sqrt 2 \<notin> Q; |
|
113 \<forall>x y z. sqrt x * sqrt x = x \<and> |
|
114 x ^ 2 = x * x \<and> |
|
115 (x ^ y) ^ z = x ^ (y*z) |
|
116 \<rbrakk> \<Longrightarrow> \<exists>a b. a \<notin> Q \<and> b \<notin> Q \<and> a ^ b \<in> Q" |
|
117 (* |
|
118 apply(case_tac "") |
|
119 apply blast |
|
120 apply(rule_tac x = "" in exI) |
|
121 apply(rule_tac x = "" in exI) |
|
122 apply simp |
|
123 done |
|
124 *) |
|
125 oops |
|
126 end |