19819
|
1 |
(* Title: FOL/ex/Intro.thy
|
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
3 |
Copyright 1992 University of Cambridge
|
|
4 |
|
|
5 |
Derives some inference rules, illustrating the use of definitions.
|
|
6 |
*)
|
|
7 |
|
60770
|
8 |
section \<open>Examples for the manual ``Introduction to Isabelle''\<close>
|
19819
|
9 |
|
|
10 |
theory Intro
|
|
11 |
imports FOL
|
|
12 |
begin
|
|
13 |
|
60770
|
14 |
subsubsection \<open>Some simple backward proofs\<close>
|
19819
|
15 |
|
69590
|
16 |
lemma mythm: \<open>P \<or> P \<longrightarrow> P\<close>
|
19819
|
17 |
apply (rule impI)
|
|
18 |
apply (rule disjE)
|
|
19 |
prefer 3 apply (assumption)
|
|
20 |
prefer 2 apply (assumption)
|
|
21 |
apply assumption
|
|
22 |
done
|
|
23 |
|
69590
|
24 |
lemma \<open>(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R)\<close>
|
19819
|
25 |
apply (rule impI)
|
|
26 |
apply (erule disjE)
|
|
27 |
apply (drule conjunct1)
|
|
28 |
apply (rule disjI1)
|
|
29 |
apply (rule_tac [2] disjI2)
|
|
30 |
apply assumption+
|
|
31 |
done
|
|
32 |
|
62020
|
33 |
text \<open>Correct version, delaying use of \<open>spec\<close> until last.\<close>
|
69590
|
34 |
lemma \<open>(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>z w. P(w,z))\<close>
|
19819
|
35 |
apply (rule impI)
|
|
36 |
apply (rule allI)
|
|
37 |
apply (rule allI)
|
|
38 |
apply (drule spec)
|
|
39 |
apply (drule spec)
|
|
40 |
apply assumption
|
|
41 |
done
|
|
42 |
|
|
43 |
|
62020
|
44 |
subsubsection \<open>Demonstration of \<open>fast\<close>\<close>
|
19819
|
45 |
|
69590
|
46 |
lemma \<open>(\<exists>y. \<forall>x. J(y,x) \<longleftrightarrow> \<not> J(x,x)) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. J(z,y) \<longleftrightarrow> \<not> J(z,x))\<close>
|
19819
|
47 |
apply fast
|
|
48 |
done
|
|
49 |
|
|
50 |
|
69590
|
51 |
lemma \<open>\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))\<close>
|
19819
|
52 |
apply fast
|
|
53 |
done
|
|
54 |
|
|
55 |
|
60770
|
56 |
subsubsection \<open>Derivation of conjunction elimination rule\<close>
|
19819
|
57 |
|
|
58 |
lemma
|
69590
|
59 |
assumes major: \<open>P \<and> Q\<close>
|
|
60 |
and minor: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close>
|
|
61 |
shows \<open>R\<close>
|
19819
|
62 |
apply (rule minor)
|
|
63 |
apply (rule major [THEN conjunct1])
|
|
64 |
apply (rule major [THEN conjunct2])
|
|
65 |
done
|
|
66 |
|
|
67 |
|
60770
|
68 |
subsection \<open>Derived rules involving definitions\<close>
|
19819
|
69 |
|
60770
|
70 |
text \<open>Derivation of negation introduction\<close>
|
19819
|
71 |
|
|
72 |
lemma
|
69590
|
73 |
assumes \<open>P \<Longrightarrow> False\<close>
|
|
74 |
shows \<open>\<not> P\<close>
|
19819
|
75 |
apply (unfold not_def)
|
|
76 |
apply (rule impI)
|
41526
|
77 |
apply (rule assms)
|
19819
|
78 |
apply assumption
|
|
79 |
done
|
|
80 |
|
|
81 |
lemma
|
69590
|
82 |
assumes major: \<open>\<not> P\<close>
|
|
83 |
and minor: \<open>P\<close>
|
|
84 |
shows \<open>R\<close>
|
19819
|
85 |
apply (rule FalseE)
|
|
86 |
apply (rule mp)
|
|
87 |
apply (rule major [unfolded not_def])
|
|
88 |
apply (rule minor)
|
|
89 |
done
|
|
90 |
|
60770
|
91 |
text \<open>Alternative proof of the result above\<close>
|
19819
|
92 |
lemma
|
69590
|
93 |
assumes major: \<open>\<not> P\<close>
|
|
94 |
and minor: \<open>P\<close>
|
|
95 |
shows \<open>R\<close>
|
19819
|
96 |
apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
|
|
97 |
done
|
|
98 |
|
|
99 |
end
|