12 definition of the propositional tautologies. |
12 definition of the propositional tautologies. |
13 |
13 |
14 Inductive definition of propositional logic. Soundness and |
14 Inductive definition of propositional logic. Soundness and |
15 completeness w.r.t.\ truth-tables. |
15 completeness w.r.t.\ truth-tables. |
16 |
16 |
17 Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in> |
17 Prove: If \<open>H |= p\<close> then \<open>G |= p\<close> where \<open>G \<in> |
18 Fin(H)"} |
18 Fin(H)\<close> |
19 \<close> |
19 \<close> |
20 |
20 |
21 |
21 |
22 subsection \<open>The datatype of propositions\<close> |
22 subsection \<open>The datatype of propositions\<close> |
23 |
23 |
64 "is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)" |
64 "is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)" |
65 |
65 |
66 definition |
66 definition |
67 is_true :: "[i,i] => o" where |
67 is_true :: "[i,i] => o" where |
68 "is_true(p,t) == is_true_fun(p,t) = 1" |
68 "is_true(p,t) == is_true_fun(p,t) = 1" |
69 -- \<open>this definition is required since predicates can't be recursive\<close> |
69 \<comment> \<open>this definition is required since predicates can't be recursive\<close> |
70 |
70 |
71 lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False" |
71 lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False" |
72 by (simp add: is_true_def) |
72 by (simp add: is_true_def) |
73 |
73 |
74 lemma is_true_Var [simp]: "is_true(#v,t) \<longleftrightarrow> v \<in> t" |
74 lemma is_true_Var [simp]: "is_true(#v,t) \<longleftrightarrow> v \<in> t" |
79 |
79 |
80 |
80 |
81 subsubsection \<open>Logical consequence\<close> |
81 subsubsection \<open>Logical consequence\<close> |
82 |
82 |
83 text \<open> |
83 text \<open> |
84 For every valuation, if all elements of @{text H} are true then so |
84 For every valuation, if all elements of \<open>H\<close> are true then so |
85 is @{text p}. |
85 is \<open>p\<close>. |
86 \<close> |
86 \<close> |
87 |
87 |
88 definition |
88 definition |
89 logcon :: "[i,i] => o" (infixl "|=" 50) where |
89 logcon :: "[i,i] => o" (infixl "|=" 50) where |
90 "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)" |
90 "H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)" |
91 |
91 |
92 |
92 |
93 text \<open> |
93 text \<open> |
94 A finite set of hypotheses from @{text t} and the @{text Var}s in |
94 A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in |
95 @{text p}. |
95 \<open>p\<close>. |
96 \<close> |
96 \<close> |
97 |
97 |
98 consts |
98 consts |
99 hyps :: "[i,i] => i" |
99 hyps :: "[i,i] => i" |
100 primrec |
100 primrec |
116 lemmas thms_in_pl = thms.dom_subset [THEN subsetD] |
116 lemmas thms_in_pl = thms.dom_subset [THEN subsetD] |
117 |
117 |
118 inductive_cases ImpE: "p=>q \<in> propn" |
118 inductive_cases ImpE: "p=>q \<in> propn" |
119 |
119 |
120 lemma thms_MP: "[| H |- p=>q; H |- p |] ==> H |- q" |
120 lemma thms_MP: "[| H |- p=>q; H |- p |] ==> H |- q" |
121 -- \<open>Stronger Modus Ponens rule: no typechecking!\<close> |
121 \<comment> \<open>Stronger Modus Ponens rule: no typechecking!\<close> |
122 apply (rule thms.MP) |
122 apply (rule thms.MP) |
123 apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+ |
123 apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+ |
124 done |
124 done |
125 |
125 |
126 lemma thms_I: "p \<in> propn ==> H |- p=>p" |
126 lemma thms_I: "p \<in> propn ==> H |- p=>p" |
127 -- \<open>Rule is called @{text I} for Identity Combinator, not for Introduction.\<close> |
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]) |
128 apply (rule thms.S [THEN thms_MP, THEN thms_MP]) |
129 apply (rule_tac [5] thms.K) |
129 apply (rule_tac [5] thms.K) |
130 apply (rule_tac [4] thms.K) |
130 apply (rule_tac [4] thms.K) |
131 apply simp_all |
131 apply simp_all |
132 done |
132 done |
133 |
133 |
134 |
134 |
135 subsubsection \<open>Weakening, left and right\<close> |
135 subsubsection \<open>Weakening, left and right\<close> |
136 |
136 |
137 lemma weaken_left: "[| G \<subseteq> H; G|-p |] ==> H|-p" |
137 lemma weaken_left: "[| G \<subseteq> H; G|-p |] ==> H|-p" |
138 -- \<open>Order of premises is convenient with @{text THEN}\<close> |
138 \<comment> \<open>Order of premises is convenient with \<open>THEN\<close>\<close> |
139 by (erule thms_mono [THEN subsetD]) |
139 by (erule thms_mono [THEN subsetD]) |
140 |
140 |
141 lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p" |
141 lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p" |
142 by (erule subset_consI [THEN weaken_left]) |
142 by (erule subset_consI [THEN weaken_left]) |
143 |
143 |
206 apply (blast intro: weaken_left_cons elim: ImpE)+ |
206 apply (blast intro: weaken_left_cons elim: ImpE)+ |
207 done |
207 done |
208 |
208 |
209 lemma hyps_thms_if: |
209 lemma hyps_thms_if: |
210 "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)" |
210 "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)" |
211 -- \<open>Typical example of strengthening the induction statement.\<close> |
211 \<comment> \<open>Typical example of strengthening the induction statement.\<close> |
212 apply simp |
212 apply simp |
213 apply (induct_tac p) |
213 apply (induct_tac p) |
214 apply (simp_all add: thms_I thms.H) |
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]) |
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)+ |
216 apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+ |
217 done |
217 done |
218 |
218 |
219 lemma logcon_thms_p: "[| p \<in> propn; 0 |= p |] ==> hyps(p,t) |- p" |
219 lemma logcon_thms_p: "[| p \<in> propn; 0 |= p |] ==> hyps(p,t) |- p" |
220 -- \<open>Key lemma for completeness; yields a set of assumptions satisfying @{text p}\<close> |
220 \<comment> \<open>Key lemma for completeness; yields a set of assumptions satisfying \<open>p\<close>\<close> |
221 apply (drule hyps_thms_if) |
221 apply (drule hyps_thms_if) |
222 apply (simp add: logcon_def) |
222 apply (simp add: logcon_def) |
223 done |
223 done |
224 |
224 |
225 text \<open> |
225 text \<open> |
240 apply (best intro!: propn_SIs intro: propn_Is)+ |
240 apply (best intro!: propn_SIs intro: propn_Is)+ |
241 done |
241 done |
242 |
242 |
243 lemma thms_excluded_middle_rule: |
243 lemma thms_excluded_middle_rule: |
244 "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \<in> propn |] ==> H |- q" |
244 "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \<in> propn |] ==> H |- q" |
245 -- \<open>Hard to prove directly because it requires cuts\<close> |
245 \<comment> \<open>Hard to prove directly because it requires cuts\<close> |
246 apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP]) |
246 apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP]) |
247 apply (blast intro!: propn_SIs intro: propn_Is)+ |
247 apply (blast intro!: propn_SIs intro: propn_Is)+ |
248 done |
248 done |
249 |
249 |
250 |
250 |
266 |
266 |
267 lemma hyps_cons: |
267 lemma hyps_cons: |
268 "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})" |
268 "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})" |
269 by (induct set: propn) auto |
269 by (induct set: propn) auto |
270 |
270 |
271 text \<open>Two lemmas for use with @{text weaken_left}\<close> |
271 text \<open>Two lemmas for use with \<open>weaken_left\<close>\<close> |
272 |
272 |
273 lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))" |
273 lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))" |
274 by blast |
274 by blast |
275 |
275 |
276 lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))" |
276 lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))" |
315 |
315 |
316 |
316 |
317 subsubsection \<open>Completeness theorem\<close> |
317 subsubsection \<open>Completeness theorem\<close> |
318 |
318 |
319 lemma completeness_0: "[| p \<in> propn; 0 |= p |] ==> 0 |- p" |
319 lemma completeness_0: "[| p \<in> propn; 0 |= p |] ==> 0 |- p" |
320 -- \<open>The base case for completeness\<close> |
320 \<comment> \<open>The base case for completeness\<close> |
321 apply (rule Diff_cancel [THEN subst]) |
321 apply (rule Diff_cancel [THEN subst]) |
322 apply (blast intro: completeness_0_lemma) |
322 apply (blast intro: completeness_0_lemma) |
323 done |
323 done |
324 |
324 |
325 lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q" |
325 lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q" |
326 -- \<open>A semantic analogue of the Deduction Theorem\<close> |
326 \<comment> \<open>A semantic analogue of the Deduction Theorem\<close> |
327 by (simp add: logcon_def) |
327 by (simp add: logcon_def) |
328 |
328 |
329 lemma completeness: |
329 lemma completeness: |
330 "H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p" |
330 "H \<in> Fin(propn) ==> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p" |
331 apply (induct arbitrary: p set: Fin) |
331 apply (induct arbitrary: p set: Fin) |