diff -r fb073a34b537 -r 8b9845807f77 src/ZF/Induct/PropLog.thy --- a/src/ZF/Induct/PropLog.thy Sat Dec 29 18:35:27 2001 +0100 +++ b/src/ZF/Induct/PropLog.thy Sat Dec 29 18:36:12 2001 +0100 @@ -2,296 +2,339 @@ ID: $Id$ Author: Tobias Nipkow & Lawrence C Paulson Copyright 1993 University of Cambridge - -Datatype definition of propositional logic formulae and inductive definition -of the propositional tautologies. +*) -Inductive definition of propositional logic. -Soundness and completeness w.r.t. truth-tables. - -Prove: If H|=p then G|=p where G \ Fin(H) -*) +header {* Meta-theory of propositional logic *} theory PropLog = Main: -(** The datatype of propositions; note mixfix syntax **) -consts - propn :: "i" +text {* + Datatype definition of propositional logic formulae and inductive + definition of the propositional tautologies. + + Inductive definition of propositional logic. Soundness and + completeness w.r.t.\ truth-tables. -datatype - "propn" = Fls - | Var ("n \ nat") ("#_" [100] 100) - | "=>" ("p \ propn", "q \ propn") (infixr 90) + Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \ + Fin(H)"} +*} + + +subsection {* The datatype of propositions *} -(** The proof system **) consts - thms :: "i => i" + propn :: i -syntax - "|-" :: "[i,i] => o" (infixl 50) +datatype propn = + Fls + | Var ("n \ nat") ("#_" [100] 100) + | Imp ("p \ propn", "q \ propn") (infixr "=>" 90) + -translations - "H |- p" == "p \ thms(H)" +subsection {* The proof system *} + +consts thms :: "i => i" +syntax "_thms" :: "[i,i] => o" (infixl "|-" 50) +translations "H |- p" == "p \ thms(H)" inductive - domains "thms(H)" <= "propn" + domains "thms(H)" \ "propn" intros H: "[| p \ H; p \ propn |] ==> H |- p" K: "[| p \ propn; q \ propn |] ==> H |- p=>q=>p" - S: "[| p \ propn; q \ propn; r \ propn |] + S: "[| p \ propn; q \ propn; r \ propn |] ==> H |- (p=>q=>r) => (p=>q) => p=>r" DN: "p \ propn ==> H |- ((p=>Fls) => Fls) => p" MP: "[| H |- p=>q; H |- p; p \ propn; q \ propn |] ==> H |- q" type_intros "propn.intros" - -(** The semantics **) -consts - "|=" :: "[i,i] => o" (infixl 50) - hyps :: "[i,i] => i" - is_true_fun :: "[i,i] => i" - -constdefs (*this definitionis necessary since predicates can't be recursive*) - is_true :: "[i,i] => o" - "is_true(p,t) == is_true_fun(p,t)=1" - -defs - (*Logical consequence: for every valuation, if all elements of H are true - then so is p*) - logcon_def: "H |= p == \t. (\q \ H. is_true(q,t)) --> is_true(p,t)" - -primrec (** A finite set of hypotheses from t and the Vars in p **) - "hyps(Fls, t) = 0" - "hyps(Var(v), t) = (if v \ t then {#v} else {#v=>Fls})" - "hyps(p=>q, t) = hyps(p,t) Un hyps(q,t)" - -primrec (** Semantics of propositional logic **) - "is_true_fun(Fls, t) = 0" - "is_true_fun(Var(v), t) = (if v \ t then 1 else 0)" - "is_true_fun(p=>q, t) = (if is_true_fun(p,t)=1 then is_true_fun(q,t) - else 1)" - declare propn.intros [simp] -(*** Semantics of propositional logic ***) + +subsection {* The semantics *} + +subsubsection {* Semantics of propositional logic. *} -(** The function is_true **) +consts + is_true_fun :: "[i,i] => i" +primrec + "is_true_fun(Fls, t) = 0" + "is_true_fun(Var(v), t) = (if v \ t then 1 else 0)" + "is_true_fun(p=>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)" + +constdefs + is_true :: "[i,i] => o" + "is_true(p,t) == is_true_fun(p,t) = 1" + -- {* this definition is required since predicates can't be recursive *} lemma is_true_Fls [simp]: "is_true(Fls,t) <-> False" -by (simp add: is_true_def) + by (simp add: is_true_def) lemma is_true_Var [simp]: "is_true(#v,t) <-> v \ t" -by (simp add: is_true_def) + by (simp add: is_true_def) lemma is_true_Imp [simp]: "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))" -by (simp add: is_true_def) + by (simp add: is_true_def) + + +subsubsection {* Logical consequence *} + +text {* + For every valuation, if all elements of @{text H} are true then so + is @{text p}. +*} + +constdefs + logcon :: "[i,i] => o" (infixl "|=" 50) + "H |= p == \t. (\q \ H. is_true(q,t)) --> is_true(p,t)" -(*** Proof theory of propositional logic ***) +text {* + A finite set of hypotheses from @{text t} and the @{text Var}s in + @{text p}. +*} + +consts + hyps :: "[i,i] => i" +primrec + "hyps(Fls, t) = 0" + "hyps(Var(v), t) = (if v \ t then {#v} else {#v=>Fls})" + "hyps(p=>q, t) = hyps(p,t) \ hyps(q,t)" + + + +subsection {* Proof theory of propositional logic *} lemma thms_mono: "G \ H ==> thms(G) \ thms(H)" -apply (unfold thms.defs ) -apply (rule lfp_mono) -apply (rule thms.bnd_mono)+ -apply (assumption | rule univ_mono basic_monos)+ -done + apply (unfold thms.defs) + apply (rule lfp_mono) + apply (rule thms.bnd_mono)+ + apply (assumption | rule univ_mono basic_monos)+ + done lemmas thms_in_pl = thms.dom_subset [THEN subsetD] inductive_cases ImpE: "p=>q \ propn" -(*Stronger Modus Ponens rule: no typechecking!*) lemma thms_MP: "[| H |- p=>q; H |- p |] ==> H |- q" -apply (rule thms.MP) -apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+ -done + -- {* Stronger Modus Ponens rule: no typechecking! *} + apply (rule thms.MP) + apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+ + done -(*Rule is called I for Identity Combinator, not for Introduction*) lemma thms_I: "p \ propn ==> H |- p=>p" -apply (rule thms.S [THEN thms_MP, THEN thms_MP]) -apply (rule_tac [5] thms.K) -apply (rule_tac [4] thms.K) -apply (simp_all add: propn.intros ) -done + -- {*Rule is called @{text I} for Identity Combinator, not for Introduction. *} + apply (rule thms.S [THEN thms_MP, THEN thms_MP]) + apply (rule_tac [5] thms.K) + apply (rule_tac [4] thms.K) + apply simp_all + done + -(** Weakening, left and right **) +subsubsection {* Weakening, left and right *} -(* [| G \ H; G|-p |] ==> H|-p Order of premises is convenient with RS*) -lemmas weaken_left = thms_mono [THEN subsetD, standard] +lemma weaken_left: "[| G \ H; G|-p |] ==> H|-p" + -- {* Order of premises is convenient with @{text THEN} *} + by (erule thms_mono [THEN subsetD]) -(* H |- p ==> cons(a,H) |- p *) -lemmas weaken_left_cons = subset_consI [THEN weaken_left] +lemma weaken_left_cons: "H |- p ==> cons(a,H) |- p" + by (erule subset_consI [THEN weaken_left]) lemmas weaken_left_Un1 = Un_upper1 [THEN weaken_left] lemmas weaken_left_Un2 = Un_upper2 [THEN weaken_left] lemma weaken_right: "[| H |- q; p \ propn |] ==> H |- p=>q" -by (simp_all add: thms.K [THEN thms_MP] thms_in_pl) + by (simp_all add: thms.K [THEN thms_MP] thms_in_pl) -(*The deduction theorem*) -lemma deduction: "[| cons(p,H) |- q; p \ propn |] ==> H |- p=>q" -apply (erule thms.induct) - apply (blast intro: thms_I thms.H [THEN weaken_right]) - apply (blast intro: thms.K [THEN weaken_right]) - apply (blast intro: thms.S [THEN weaken_right]) - apply (blast intro: thms.DN [THEN weaken_right]) -apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]]) -done +subsubsection {* The deduction theorem *} + +theorem deduction: "[| cons(p,H) |- q; p \ propn |] ==> H |- p=>q" + apply (erule thms.induct) + apply (blast intro: thms_I thms.H [THEN weaken_right]) + apply (blast intro: thms.K [THEN weaken_right]) + apply (blast intro: thms.S [THEN weaken_right]) + apply (blast intro: thms.DN [THEN weaken_right]) + apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]]) + done -(*The cut rule*) +subsubsection {* The cut rule *} + lemma cut: "[| H|-p; cons(p,H) |- q |] ==> H |- q" -apply (rule deduction [THEN thms_MP]) -apply (simp_all add: thms_in_pl) -done + apply (rule deduction [THEN thms_MP]) + apply (simp_all add: thms_in_pl) + done lemma thms_FlsE: "[| H |- Fls; p \ propn |] ==> H |- p" -apply (rule thms.DN [THEN thms_MP]) -apply (rule_tac [2] weaken_right) -apply (simp_all add: propn.intros) -done + apply (rule thms.DN [THEN thms_MP]) + apply (rule_tac [2] weaken_right) + apply (simp_all add: propn.intros) + done -(* [| H |- p=>Fls; H |- p; q \ propn |] ==> H |- q *) -lemmas thms_notE = thms_MP [THEN thms_FlsE, standard] +lemma thms_notE: "[| H |- p=>Fls; H |- p; q \ propn |] ==> H |- q" + by (erule thms_MP [THEN thms_FlsE]) + + +subsubsection {* Soundness of the rules wrt truth-table semantics *} -(*Soundness of the rules wrt truth-table semantics*) -lemma soundness: "H |- p ==> H |= p" -apply (unfold logcon_def) -apply (erule thms.induct) -apply auto -done +theorem soundness: "H |- p ==> H |= p" + apply (unfold logcon_def) + apply (erule thms.induct) + apply auto + done -(*** Towards the completeness proof ***) + +subsection {* Completeness *} + +subsubsection {* Towards the completeness proof *} lemma Fls_Imp: "[| H |- p=>Fls; q \ propn |] ==> H |- p=>q" -apply (frule thms_in_pl) -apply (rule deduction) -apply (rule weaken_left_cons [THEN thms_notE]) -apply (blast intro: thms.H elim: ImpE)+ -done + apply (frule thms_in_pl) + apply (rule deduction) + apply (rule weaken_left_cons [THEN thms_notE]) + apply (blast intro: thms.H elim: ImpE)+ + done lemma Imp_Fls: "[| H |- p; H |- q=>Fls |] ==> H |- (p=>q)=>Fls" -apply (frule thms_in_pl) -apply (frule thms_in_pl [of concl: "q=>Fls"]) -apply (rule deduction) -apply (erule weaken_left_cons [THEN thms_MP]) -apply (rule consI1 [THEN thms.H, THEN thms_MP]) -apply (blast intro: weaken_left_cons elim: ImpE)+ -done + apply (frule thms_in_pl) + apply (frule thms_in_pl [of concl: "q=>Fls"]) + apply (rule deduction) + apply (erule weaken_left_cons [THEN thms_MP]) + apply (rule consI1 [THEN thms.H, THEN thms_MP]) + apply (blast intro: weaken_left_cons elim: ImpE)+ + done -(*Typical example of strengthening the induction formula*) lemma hyps_thms_if: - "p \ propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)" -apply (simp (no_asm)) -apply (induct_tac "p") -apply (simp_all (no_asm_simp) add: thms_I thms.H) -apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] - Fls_Imp [THEN weaken_left_Un2]) -apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+ -done + "p \ propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)" + -- {* Typical example of strengthening the induction statement. *} + apply simp + apply (induct_tac p) + apply (simp_all add: thms_I thms.H) + apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] Fls_Imp [THEN weaken_left_Un2]) + apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+ + done + +lemma logcon_thms_p: "[| p \ propn; 0 |= p |] ==> hyps(p,t) |- p" + -- {* Key lemma for completeness; yields a set of assumptions satisfying @{text p} *} + apply (drule hyps_thms_if) + apply (simp add: logcon_def) + done + +text {* + For proving certain theorems in our new propositional logic. +*} -(*Key lemma for completeness; yields a set of assumptions satisfying p*) -lemma logcon_thms_p: "[| p \ propn; 0 |= p |] ==> hyps(p,t) |- p" -apply (unfold logcon_def) -apply (drule hyps_thms_if) -apply simp -done +lemmas propn_SIs = propn.intros deduction + and propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP] + +text {* + The excluded middle in the form of an elimination rule. +*} +lemma thms_excluded_middle: + "[| p \ propn; q \ propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q" + apply (rule deduction [THEN deduction]) + apply (rule thms.DN [THEN thms_MP]) + apply (best intro!: propn_SIs intro: propn_Is)+ + done -(*For proving certain theorems in our new propositional logic*) -lemmas propn_SIs = propn.intros deduction -lemmas propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP] +lemma thms_excluded_middle_rule: + "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \ propn |] ==> H |- q" + -- {* Hard to prove directly because it requires cuts *} + apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP]) + apply (blast intro!: propn_SIs intro: propn_Is)+ + done -(*The excluded middle in the form of an elimination rule*) -lemma thms_excluded_middle: - "[| p \ propn; q \ propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q" -apply (rule deduction [THEN deduction]) -apply (rule thms.DN [THEN thms_MP]) -apply (best intro!: propn_SIs intro: propn_Is)+ -done +subsubsection {* Completeness -- lemmas for reducing the set of assumptions *} -(*Hard to prove directly because it requires cuts*) -lemma thms_excluded_middle_rule: - "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \ propn |] ==> H |- q" -apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP]) -apply (blast intro!: propn_SIs intro: propn_Is)+ -done +text {* + For the case @{prop "hyps(p,t)-cons(#v,Y) |- p"} we also have @{prop + "hyps(p,t)-{#v} \ hyps(p, t-{v})"}. +*} +lemma hyps_Diff: + "p \ propn ==> hyps(p, t-{v}) \ cons(#v=>Fls, hyps(p,t)-{#v})" + by (induct_tac p) auto -(*** Completeness -- lemmas for reducing the set of assumptions ***) - -(*For the case hyps(p,t)-cons(#v,Y) |- p - we also have hyps(p,t)-{#v} \ hyps(p, t-{v}) *) -lemma hyps_Diff: - "p \ propn ==> hyps(p, t-{v}) \ cons(#v=>Fls, hyps(p,t)-{#v})" -by (induct_tac "p", auto) +text {* + For the case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} we also have + @{prop "hyps(p,t)-{#v=>Fls} \ hyps(p, cons(v,t))"}. +*} -(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p - we also have hyps(p,t)-{#v=>Fls} \ hyps(p, cons(v,t)) *) lemma hyps_cons: - "p \ propn ==> hyps(p, cons(v,t)) \ cons(#v, hyps(p,t)-{#v=>Fls})" -by (induct_tac "p", auto) + "p \ propn ==> hyps(p, cons(v,t)) \ cons(#v, hyps(p,t)-{#v=>Fls})" + by (induct_tac p) auto -(** Two lemmas for use with weaken_left **) +text {* Two lemmas for use with @{text weaken_left} *} lemma cons_Diff_same: "B-C \ cons(a, B-cons(a,C))" -by blast + by blast lemma cons_Diff_subset2: "cons(a, B-{c}) - D \ cons(a, B-cons(c,D))" -by blast + by blast -(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls - could probably prove the stronger hyps(p,t) \ Fin(hyps(p,0) Un hyps(p,nat))*) +text {* + The set @{term "hyps(p,t)"} is finite, and elements have the form + @{term "#v"} or @{term "#v=>Fls"}; could probably prove the stronger + @{prop "hyps(p,t) \ Fin(hyps(p,0) \ hyps(p,nat))"}. +*} + lemma hyps_finite: "p \ propn ==> hyps(p,t) \ Fin(\v \ nat. {#v, #v=>Fls})" -by (induct_tac "p", auto) + by (induct_tac p) auto lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left] -(*Induction on the finite set of assumptions hyps(p,t0). - We may repeatedly subtract assumptions until none are left!*) +text {* + Induction on the finite set of assumptions @{term "hyps(p,t0)"}. We + may repeatedly subtract assumptions until none are left! +*} + lemma completeness_0_lemma [rule_format]: "[| p \ propn; 0 |= p |] ==> \t. hyps(p,t) - hyps(p,t0) |- p" -apply (frule hyps_finite) -apply (erule Fin_induct) -apply (simp add: logcon_thms_p Diff_0) -(*inductive step*) -apply safe -(*Case hyps(p,t)-cons(#v,Y) |- p *) - apply (rule thms_excluded_middle_rule) - apply (erule_tac [3] propn.intros) + apply (frule hyps_finite) + apply (erule Fin_induct) + apply (simp add: logcon_thms_p Diff_0) + txt {* inductive step *} + apply safe + txt {* Case @{prop "hyps(p,t)-cons(#v,Y) |- p"} *} + apply (rule thms_excluded_middle_rule) + apply (erule_tac [3] propn.intros) + apply (blast intro: cons_Diff_same [THEN weaken_left]) + apply (blast intro: cons_Diff_subset2 [THEN weaken_left] + hyps_Diff [THEN Diff_weaken_left]) + txt {* Case @{prop "hyps(p,t)-cons(#v => Fls,Y) |- p"} *} + apply (rule thms_excluded_middle_rule) + apply (erule_tac [3] propn.intros) + apply (blast intro: cons_Diff_subset2 [THEN weaken_left] + hyps_cons [THEN Diff_weaken_left]) apply (blast intro: cons_Diff_same [THEN weaken_left]) - apply (blast intro: cons_Diff_subset2 [THEN weaken_left] - hyps_Diff [THEN Diff_weaken_left]) -(*Case hyps(p,t)-cons(#v => Fls,Y) |- p *) -apply (rule thms_excluded_middle_rule) - apply (erule_tac [3] propn.intros) - apply (blast intro: cons_Diff_subset2 [THEN weaken_left] - hyps_cons [THEN Diff_weaken_left]) -apply (blast intro: cons_Diff_same [THEN weaken_left]) -done + done + + +subsubsection {* Completeness theorem *} -(*The base case for completeness*) lemma completeness_0: "[| p \ propn; 0 |= p |] ==> 0 |- p" -apply (rule Diff_cancel [THEN subst]) -apply (blast intro: completeness_0_lemma) -done + -- {* The base case for completeness *} + apply (rule Diff_cancel [THEN subst]) + apply (blast intro: completeness_0_lemma) + done -(*A semantic analogue of the Deduction Theorem*) lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q" -by (simp add: logcon_def) + -- {* A semantic analogue of the Deduction Theorem *} + by (simp add: logcon_def) lemma completeness [rule_format]: "H \ Fin(propn) ==> \p \ propn. H |= p --> H |- p" -apply (erule Fin_induct) -apply (safe intro!: completeness_0) -apply (rule weaken_left_cons [THEN thms_MP]) - apply (blast intro!: logcon_Imp propn.intros) -apply (blast intro: propn_Is) -done + apply (erule Fin_induct) + apply (safe intro!: completeness_0) + apply (rule weaken_left_cons [THEN thms_MP]) + apply (blast intro!: logcon_Imp propn.intros) + apply (blast intro: propn_Is) + done -lemma thms_iff: "H \ Fin(propn) ==> H |- p <-> H |= p & p \ propn" -by (blast intro: soundness completeness thms_in_pl) +theorem thms_iff: "H \ Fin(propn) ==> H |- p <-> H |= p \ p \ propn" + by (blast intro: soundness completeness thms_in_pl) end