1(*  Title:      ZF/Induct/PropLog.thy
2    Author:     Tobias Nipkow & Lawrence C Paulson
3    Copyright   1993  University of Cambridge
4*)
5
6section \<open>Meta-theory of propositional logic\<close>
7
8theory PropLog imports ZF begin
9
10text \<open>
11  Datatype definition of propositional logic formulae and inductive
12  definition of the propositional tautologies.
13
14  Inductive definition of propositional logic.  Soundness and
15  completeness w.r.t.\ truth-tables.
16
17  Prove: If \<open>H |= p\<close> then \<open>G |= p\<close> where \<open>G \<in>
18  Fin(H)\<close>
19\<close>
20
21
22subsection \<open>The datatype of propositions\<close>
23
24consts
25  propn :: i
26
27datatype propn =
28    Fls
29  | Var ("n \<in> nat")    (\<open>#_\<close> [100] 100)
30  | Imp ("p \<in> propn", "q \<in> propn")    (infixr \<open>=>\<close> 90)
31
32
33subsection \<open>The proof system\<close>
34
35consts thms     :: "i => i"
36
37abbreviation
38  thms_syntax :: "[i,i] => o"    (infixl \<open>|-\<close> 50)
39  where "H |- p == p \<in> thms(H)"
40
41inductive
42  domains "thms(H)" \<subseteq> "propn"
43  intros
44    H:  "[| p \<in> H;  p \<in> propn |] ==> H |- p"
45    K:  "[| p \<in> propn;  q \<in> propn |] ==> H |- p=>q=>p"
46    S:  "[| p \<in> propn;  q \<in> propn;  r \<in> propn |]
47         ==> H |- (p=>q=>r) => (p=>q) => p=>r"
48    DN: "p \<in> propn ==> H |- ((p=>Fls) => Fls) => p"
49    MP: "[| H |- p=>q;  H |- p;  p \<in> propn;  q \<in> propn |] ==> H |- q"
50  type_intros "propn.intros"
51
52declare propn.intros [simp]
53
54
55subsection \<open>The semantics\<close>
56
57subsubsection \<open>Semantics of propositional logic.\<close>
58
59consts
60  is_true_fun :: "[i,i] => i"
61primrec
62  "is_true_fun(Fls, t) = 0"
63  "is_true_fun(Var(v), t) = (if v \<in> t then 1 else 0)"
64  "is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)"
65
66definition
67  is_true :: "[i,i] => o"  where
68  "is_true(p,t) == is_true_fun(p,t) = 1"
69  \<comment> \<open>this definition is required since predicates can't be recursive\<close>
70
71lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False"
72  by (simp add: is_true_def)
73
74lemma is_true_Var [simp]: "is_true(#v,t) \<longleftrightarrow> v \<in> t"
75  by (simp add: is_true_def)
76
77lemma is_true_Imp [simp]: "is_true(p=>q,t) \<longleftrightarrow> (is_true(p,t)\<longrightarrow>is_true(q,t))"
78  by (simp add: is_true_def)
79
80
81subsubsection \<open>Logical consequence\<close>
82
83text \<open>
84  For every valuation, if all elements of \<open>H\<close> are true then so
85  is \<open>p\<close>.
86\<close>
87
88definition
89  logcon :: "[i,i] => o"    (infixl \<open>|=\<close> 50)  where
90  "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)"
91
92
93text \<open>
94  A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in
95  \<open>p\<close>.
96\<close>
97
98consts
99  hyps :: "[i,i] => i"
100primrec
101  "hyps(Fls, t) = 0"
102  "hyps(Var(v), t) = (if v \<in> t then {#v} else {#v=>Fls})"
103  "hyps(p=>q, t) = hyps(p,t) \<union> hyps(q,t)"
104
105
106
107subsection \<open>Proof theory of propositional logic\<close>
108
109lemma thms_mono: "G \<subseteq> H ==> thms(G) \<subseteq> thms(H)"
110  apply (unfold thms.defs)
111  apply (rule lfp_mono)
112    apply (rule thms.bnd_mono)+
113  apply (assumption | rule univ_mono basic_monos)+
114  done
115
116lemmas thms_in_pl = thms.dom_subset [THEN subsetD]
117
118inductive_cases ImpE: "p=>q \<in> propn"
119
120lemma thms_MP: "[| H |- p=>q;  H |- p |] ==> H |- q"
121  \<comment> \<open>Stronger Modus Ponens rule: no typechecking!\<close>
122  apply (rule thms.MP)
123     apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
124  done
125
126lemma thms_I: "p \<in> propn ==> H |- p=>p"
127  \<comment> \<open>Rule is called \<open>I\<close> for Identity Combinator, not for Introduction.\<close>
128  apply (rule thms.S [THEN thms_MP, THEN thms_MP])
129      apply (rule_tac [5] thms.K)
130       apply (rule_tac [4] thms.K)
131         apply simp_all
132  done
133
134
135subsubsection \<open>Weakening, left and right\<close>
136
137lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
138  \<comment> \<open>Order of premises is convenient with \<open>THEN\<close>\<close>
139  by (erule thms_mono [THEN subsetD])
140
141lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p"
142  by (erule subset_consI [THEN weaken_left])
143
144lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
145lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]
146
147lemma weaken_right: "[| H |- q;  p \<in> propn |] ==> H |- p=>q"
148  by (simp_all add: thms.K [THEN thms_MP] thms_in_pl)
149
150
151subsubsection \<open>The deduction theorem\<close>
152
153theorem deduction: "[| cons(p,H) |- q;  p \<in> propn |] ==>  H |- p=>q"
154  apply (erule thms.induct)
155      apply (blast intro: thms_I thms.H [THEN weaken_right])
156     apply (blast intro: thms.K [THEN weaken_right])
157    apply (blast intro: thms.S [THEN weaken_right])
158   apply (blast intro: thms.DN [THEN weaken_right])
159  apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
160  done
161
162
163subsubsection \<open>The cut rule\<close>
164
165lemma cut: "[| H|-p;  cons(p,H) |- q |] ==>  H |- q"
166  apply (rule deduction [THEN thms_MP])
167    apply (simp_all add: thms_in_pl)
168  done
169
170lemma thms_FlsE: "[| H |- Fls; p \<in> propn |] ==> H |- p"
171  apply (rule thms.DN [THEN thms_MP])
172   apply (rule_tac [2] weaken_right)
173    apply (simp_all add: propn.intros)
174  done
175
176lemma thms_notE: "[| H |- p=>Fls;  H |- p;  q \<in> propn |] ==> H |- q"
177  by (erule thms_MP [THEN thms_FlsE])
178
179
180subsubsection \<open>Soundness of the rules wrt truth-table semantics\<close>
181
182theorem soundness: "H |- p ==> H |= p"
183  apply (unfold logcon_def)
184  apply (induct set: thms)
185      apply auto
186  done
187
188
189subsection \<open>Completeness\<close>
190
191subsubsection \<open>Towards the completeness proof\<close>
192
193lemma Fls_Imp: "[| H |- p=>Fls; q \<in> propn |] ==> H |- p=>q"
194  apply (frule thms_in_pl)
195  apply (rule deduction)
196   apply (rule weaken_left_cons [THEN thms_notE])
197     apply (blast intro: thms.H elim: ImpE)+
198  done
199
200lemma Imp_Fls: "[| H |- p;  H |- q=>Fls |] ==> H |- (p=>q)=>Fls"
201  apply (frule thms_in_pl)
202  apply (frule thms_in_pl [of concl: "q=>Fls"])
203  apply (rule deduction)
204   apply (erule weaken_left_cons [THEN thms_MP])
205   apply (rule consI1 [THEN thms.H, THEN thms_MP])
206    apply (blast intro: weaken_left_cons elim: ImpE)+
207  done
208
209lemma hyps_thms_if:
210    "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
211  \<comment> \<open>Typical example of strengthening the induction statement.\<close>
212  apply simp
213  apply (induct_tac p)
214    apply (simp_all add: thms_I thms.H)
215  apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] Fls_Imp [THEN weaken_left_Un2])
216  apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
217  done
218
219lemma logcon_thms_p: "[| p \<in> propn;  0 |= p |] ==> hyps(p,t) |- p"
220  \<comment> \<open>Key lemma for completeness; yields a set of assumptions satisfying \<open>p\<close>\<close>
221  apply (drule hyps_thms_if)
222  apply (simp add: logcon_def)
223  done
224
225text \<open>
226  For proving certain theorems in our new propositional logic.
227\<close>
228
229lemmas propn_SIs = propn.intros deduction
230  and propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]
231
232text \<open>
233  The excluded middle in the form of an elimination rule.
234\<close>
235
236lemma thms_excluded_middle:
237    "[| p \<in> propn;  q \<in> propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"
238  apply (rule deduction [THEN deduction])
239    apply (rule thms.DN [THEN thms_MP])
240     apply (best intro!: propn_SIs intro: propn_Is)+
241  done
242
243lemma thms_excluded_middle_rule:
244  "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p \<in> propn |] ==> H |- q"
245  \<comment> \<open>Hard to prove directly because it requires cuts\<close>
246  apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
247     apply (blast intro!: propn_SIs intro: propn_Is)+
248  done
249
250
251subsubsection \<open>Completeness -- lemmas for reducing the set of assumptions\<close>
252
253text \<open>
254  For the case \<^prop>\<open>hyps(p,t)-cons(#v,Y) |- p\<close> we also have \<^prop>\<open>hyps(p,t)-{#v} \<subseteq> hyps(p, t-{v})\<close>.
255\<close>
256
257lemma hyps_Diff:
258    "p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"
259  by (induct set: propn) auto
260
261text \<open>
262  For the case \<^prop>\<open>hyps(p,t)-cons(#v => Fls,Y) |- p\<close> we also have
263  \<^prop>\<open>hyps(p,t)-{#v=>Fls} \<subseteq> hyps(p, cons(v,t))\<close>.
264\<close>
265
266lemma hyps_cons:
267    "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
268  by (induct set: propn) auto
269
270text \<open>Two lemmas for use with \<open>weaken_left\<close>\<close>
271
272lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
273  by blast
274
275lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))"
276  by blast
277
278text \<open>
279  The set \<^term>\<open>hyps(p,t)\<close> is finite, and elements have the form
280  \<^term>\<open>#v\<close> or \<^term>\<open>#v=>Fls\<close>; could probably prove the stronger
281  \<^prop>\<open>hyps(p,t) \<in> Fin(hyps(p,0) \<union> hyps(p,nat))\<close>.
282\<close>
283
284lemma hyps_finite: "p \<in> propn ==> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v=>Fls})"
285  by (induct set: propn) auto
286
287lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
288
289text \<open>
290  Induction on the finite set of assumptions \<^term>\<open>hyps(p,t0)\<close>.  We
291  may repeatedly subtract assumptions until none are left!
292\<close>
293
294lemma completeness_0_lemma [rule_format]:
295    "[| p \<in> propn;  0 |= p |] ==> \<forall>t. hyps(p,t) - hyps(p,t0) |- p"
296  apply (frule hyps_finite)
297  apply (erule Fin_induct)
298   apply (simp add: logcon_thms_p Diff_0)
299  txt \<open>inductive step\<close>
300  apply safe
301   txt \<open>Case \<^prop>\<open>hyps(p,t)-cons(#v,Y) |- p\<close>\<close>
302   apply (rule thms_excluded_middle_rule)
303     apply (erule_tac [3] propn.intros)
304    apply (blast intro: cons_Diff_same [THEN weaken_left])
305   apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
306     hyps_Diff [THEN Diff_weaken_left])
307  txt \<open>Case \<^prop>\<open>hyps(p,t)-cons(#v => Fls,Y) |- p\<close>\<close>
308  apply (rule thms_excluded_middle_rule)
309    apply (erule_tac [3] propn.intros)
310   apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
311     hyps_cons [THEN Diff_weaken_left])
312  apply (blast intro: cons_Diff_same [THEN weaken_left])
313  done
314
315
316subsubsection \<open>Completeness theorem\<close>
317
318lemma completeness_0: "[| p \<in> propn;  0 |= p |] ==> 0 |- p"
319  \<comment> \<open>The base case for completeness\<close>
320  apply (rule Diff_cancel [THEN subst])
321  apply (blast intro: completeness_0_lemma)
322  done
323
324lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
325  \<comment> \<open>A semantic analogue of the Deduction Theorem\<close>
326  by (simp add: logcon_def)
327
328lemma completeness:
329     "H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p"
330  apply (induct arbitrary: p set: Fin)
331   apply (safe intro!: completeness_0)
332  apply (rule weaken_left_cons [THEN thms_MP])
333   apply (blast intro!: logcon_Imp propn.intros)
334  apply (blast intro: propn_Is)
335  done
336
337theorem thms_iff: "H \<in> Fin(propn) ==> H |- p \<longleftrightarrow> H |= p \<and> p \<in> propn"
338  by (blast intro: soundness completeness thms_in_pl)
339
340end
341