equal
deleted
inserted
replaced
6 |
6 |
7 theory Structured_Statements |
7 theory Structured_Statements |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
|
11 subsection \<open>Introduction steps\<close> |
|
12 |
11 notepad |
13 notepad |
12 begin |
14 begin |
|
15 fix A B :: bool |
|
16 fix P :: "'a \<Rightarrow> bool" |
13 |
17 |
|
18 have "A \<longrightarrow> B" |
|
19 proof |
|
20 show B if A using that sorry |
|
21 qed |
|
22 |
|
23 have "\<not> A" |
|
24 proof |
|
25 show False if A using that sorry |
|
26 qed |
|
27 |
|
28 have "\<forall>x. P x" |
|
29 proof |
|
30 show "P x" for x sorry |
|
31 qed |
|
32 end |
|
33 |
|
34 |
|
35 subsection \<open>If-and-only-if\<close> |
|
36 |
|
37 notepad |
|
38 begin |
|
39 fix A B :: bool |
|
40 |
|
41 have "A \<longleftrightarrow> B" |
|
42 proof |
|
43 show B if A sorry |
|
44 show A if B sorry |
|
45 qed |
|
46 next |
14 fix A B :: bool |
47 fix A B :: bool |
15 |
48 |
16 have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)" |
49 have iff_comm: "(A \<and> B) \<longleftrightarrow> (B \<and> A)" |
17 proof |
50 proof |
18 show "B \<and> A" if "A \<and> B" |
51 show "B \<and> A" if "A \<and> B" |
36 show A using that .. |
69 show A using that .. |
37 qed |
70 qed |
38 then show "A \<and> B" if "B \<and> A" |
71 then show "A \<and> B" if "B \<and> A" |
39 by this (rule that) |
72 by this (rule that) |
40 qed |
73 qed |
|
74 end |
41 |
75 |
|
76 |
|
77 subsection \<open>Elimination and cases\<close> |
|
78 |
|
79 notepad |
|
80 begin |
|
81 fix A B C D :: bool |
|
82 assume *: "A \<or> B \<or> C \<or> D" |
|
83 |
|
84 consider (a) A | (b) B | (c) C | (d) D |
|
85 using * by blast |
|
86 then have something |
|
87 proof cases |
|
88 case a thm \<open>A\<close> |
|
89 then show ?thesis sorry |
|
90 next |
|
91 case b thm \<open>B\<close> |
|
92 then show ?thesis sorry |
|
93 next |
|
94 case c thm \<open>C\<close> |
|
95 then show ?thesis sorry |
|
96 next |
|
97 case d thm \<open>D\<close> |
|
98 then show ?thesis sorry |
|
99 qed |
|
100 next |
|
101 fix A :: "'a \<Rightarrow> bool" |
|
102 fix B :: "'b \<Rightarrow> 'c \<Rightarrow> bool" |
|
103 assume *: "(\<exists>x. A x) \<or> (\<exists>y z. B y z)" |
|
104 |
|
105 consider (a) x where "A x" | (b) y z where "B y z" |
|
106 using * by blast |
|
107 then have something |
|
108 proof cases |
|
109 case a thm \<open>A x\<close> |
|
110 then show ?thesis sorry |
|
111 next |
|
112 case b thm \<open>B y z\<close> |
|
113 then show ?thesis sorry |
|
114 qed |
|
115 end |
|
116 |
|
117 |
|
118 subsection \<open>Induction\<close> |
|
119 |
|
120 notepad |
|
121 begin |
|
122 fix P :: "nat \<Rightarrow> bool" |
|
123 fix n :: nat |
|
124 |
|
125 have "P n" |
|
126 proof (induct n) |
|
127 show "P 0" sorry |
|
128 show "P (Suc n)" if "P n" for n thm \<open>P n\<close> |
|
129 using that sorry |
|
130 qed |
42 end |
131 end |
43 |
132 |
44 end |
133 end |