diff -r f04b33ce250f -r a4dc62a46ee4 ex/PropLog.ML --- a/ex/PropLog.ML Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,234 +0,0 @@ -(* Title: HOL/ex/pl.ML - ID: $Id$ - Author: Tobias Nipkow & Lawrence C Paulson - Copyright 1994 TU Muenchen & University of Cambridge - -Soundness and completeness of propositional logic w.r.t. truth-tables. - -Prove: If H|=p then G|=p where G:Fin(H) -*) - -open PropLog; - -(** Monotonicity **) -goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)"; -by (rtac lfp_mono 1); -by (REPEAT (ares_tac basic_monos 1)); -qed "thms_mono"; - -(*Rule is called I for Identity Combinator, not for Introduction*) -goal PropLog.thy "H |- p->p"; -by(best_tac (HOL_cs addIs [thms.K,thms.S,thms.MP]) 1); -qed "thms_I"; - -(** Weakening, left and right **) - -(* "[| G<=H; G |- p |] ==> H |- p" - This order of premises is convenient with RS -*) -bind_thm ("weaken_left", (thms_mono RS subsetD)); - -(* H |- p ==> insert(a,H) |- p *) -val weaken_left_insert = subset_insertI RS weaken_left; - -val weaken_left_Un1 = Un_upper1 RS weaken_left; -val weaken_left_Un2 = Un_upper2 RS weaken_left; - -goal PropLog.thy "!!H. H |- q ==> H |- p->q"; -by(fast_tac (HOL_cs addIs [thms.K,thms.MP]) 1); -qed "weaken_right"; - -(*The deduction theorem*) -goal PropLog.thy "!!H. insert(p,H) |- q ==> H |- p->q"; -by (etac thms.induct 1); -by (fast_tac (set_cs addIs [thms_I, thms.H RS weaken_right]) 1); -by (fast_tac (set_cs addIs [thms.K RS weaken_right]) 1); -by (fast_tac (set_cs addIs [thms.S RS weaken_right]) 1); -by (fast_tac (set_cs addIs [thms.DN RS weaken_right]) 1); -by (fast_tac (set_cs addIs [thms.S RS thms.MP RS thms.MP]) 1); -qed "deduction"; - - -(* "[| insert(p,H) |- q; H |- p |] ==> H |- q" - The cut rule - not used -*) -val cut = deduction RS thms.MP; - -(* H |- false ==> H |- p *) -val thms_falseE = weaken_right RS (thms.DN RS thms.MP); - -(* [| H |- p->false; H |- p; q: pl |] ==> H |- q *) -bind_thm ("thms_notE", (thms.MP RS thms_falseE)); - -(** The function eval **) - -val pl_ss = set_ss addsimps - (PropLog.pl.simps @ [eval2_false, eval2_var, eval2_imp] - @ [hyps_false, hyps_var, hyps_imp]); - -goalw PropLog.thy [eval_def] "tt[false] = False"; -by (simp_tac pl_ss 1); -qed "eval_false"; - -goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)"; -by (simp_tac pl_ss 1); -qed "eval_var"; - -goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])"; -by (simp_tac pl_ss 1); -qed "eval_imp"; - -val pl_ss = pl_ss addsimps [eval_false, eval_var, eval_imp]; - -(*Soundness of the rules wrt truth-table semantics*) -goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p"; -by (etac thms.induct 1); -by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5); -by (ALLGOALS (asm_simp_tac pl_ss)); -qed "soundness"; - -(*** Towards the completeness proof ***) - -goal PropLog.thy "!!H. H |- p->false ==> H |- p->q"; -by (rtac deduction 1); -by (etac (weaken_left_insert RS thms_notE) 1); -by (rtac thms.H 1); -by (rtac insertI1 1); -qed "false_imp"; - -val [premp,premq] = goal PropLog.thy - "[| H |- p; H |- q->false |] ==> H |- (p->q)->false"; -by (rtac deduction 1); -by (rtac (premq RS weaken_left_insert RS thms.MP) 1); -by (rtac (thms.H RS thms.MP) 1); -by (rtac insertI1 1); -by (rtac (premp RS weaken_left_insert) 1); -qed "imp_false"; - -(*This formulation is required for strong induction hypotheses*) -goal PropLog.thy "hyps(p,tt) |- if(tt[p], p, p->false)"; -by (rtac (expand_if RS iffD2) 1); -by(PropLog.pl.induct_tac "p" 1); -by (ALLGOALS (simp_tac (pl_ss addsimps [thms_I, thms.H]))); -by (fast_tac (set_cs addIs [weaken_left_Un1, weaken_left_Un2, - weaken_right, imp_false] - addSEs [false_imp]) 1); -qed "hyps_thms_if"; - -(*Key lemma for completeness; yields a set of assumptions satisfying p*) -val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps(p,tt) |- p"; -by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN - rtac hyps_thms_if 2); -by (fast_tac set_cs 1); -qed "sat_thms_p"; - -(*For proving certain theorems in our new propositional logic*) -val thms_cs = - set_cs addSIs [deduction] addIs [thms.H, thms.H RS thms.MP]; - -(*The excluded middle in the form of an elimination rule*) -goal PropLog.thy "H |- (p->q) -> ((p->false)->q) -> q"; -by (rtac (deduction RS deduction) 1); -by (rtac (thms.DN RS thms.MP) 1); -by (ALLGOALS (best_tac (thms_cs addSIs prems))); -qed "thms_excluded_middle"; - -(*Hard to prove directly because it requires cuts*) -val prems = goal PropLog.thy - "[| insert(p,H) |- q; insert(p->false,H) |- q |] ==> H |- q"; -by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1); -by (REPEAT (resolve_tac (prems@[deduction]) 1)); -qed "thms_excluded_middle_rule"; - -(*** Completeness -- lemmas for reducing the set of assumptions ***) - -(*For the case hyps(p,t)-insert(#v,Y) |- p; - we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *) -goal PropLog.thy "hyps(p, t-{v}) <= insert(#v->false, hyps(p,t)-{#v})"; -by (PropLog.pl.induct_tac "p" 1); -by (simp_tac pl_ss 1); -by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1); -by (simp_tac pl_ss 1); -by (fast_tac set_cs 1); -qed "hyps_Diff"; - -(*For the case hyps(p,t)-insert(#v -> false,Y) |- p; - we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *) -goal PropLog.thy "hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{#v->false})"; -by (PropLog.pl.induct_tac "p" 1); -by (simp_tac pl_ss 1); -by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1); -by (simp_tac pl_ss 1); -by (fast_tac set_cs 1); -qed "hyps_insert"; - -(** Two lemmas for use with weaken_left **) - -goal Set.thy "B-C <= insert(a, B-insert(a,C))"; -by (fast_tac set_cs 1); -qed "insert_Diff_same"; - -goal Set.thy "insert(a, B-{c}) - D <= insert(a, B-insert(c,D))"; -by (fast_tac set_cs 1); -qed "insert_Diff_subset2"; - -(*The set hyps(p,t) is finite, and elements have the form #v or #v->false; - could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*) -goal PropLog.thy "hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})"; -by (PropLog.pl.induct_tac "p" 1); -by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN' - fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI]))); -qed "hyps_finite"; - -val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; - -(*Induction on the finite set of assumptions hyps(p,t0). - We may repeatedly subtract assumptions until none are left!*) -val [sat] = goal PropLog.thy - "{} |= p ==> !t. hyps(p,t) - hyps(p,t0) |- p"; -by (rtac (hyps_finite RS Fin_induct) 1); -by (simp_tac (pl_ss addsimps [sat RS sat_thms_p]) 1); -by (safe_tac set_cs); -(*Case hyps(p,t)-insert(#v,Y) |- p *) -by (rtac thms_excluded_middle_rule 1); -by (rtac (insert_Diff_same RS weaken_left) 1); -by (etac spec 1); -by (rtac (insert_Diff_subset2 RS weaken_left) 1); -by (rtac (hyps_Diff RS Diff_weaken_left) 1); -by (etac spec 1); -(*Case hyps(p,t)-insert(#v -> false,Y) |- p *) -by (rtac thms_excluded_middle_rule 1); -by (rtac (insert_Diff_same RS weaken_left) 2); -by (etac spec 2); -by (rtac (insert_Diff_subset2 RS weaken_left) 1); -by (rtac (hyps_insert RS Diff_weaken_left) 1); -by (etac spec 1); -qed "completeness_0_lemma"; - -(*The base case for completeness*) -val [sat] = goal PropLog.thy "{} |= p ==> {} |- p"; -by (rtac (Diff_cancel RS subst) 1); -by (rtac (sat RS (completeness_0_lemma RS spec)) 1); -qed "completeness_0"; - -(*A semantic analogue of the Deduction Theorem*) -val [sat] = goalw PropLog.thy [sat_def] "insert(p,H) |= q ==> H |= p->q"; -by (simp_tac pl_ss 1); -by (cfast_tac [sat] 1); -qed "sat_imp"; - -val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p"; -by (rtac (finite RS Fin_induct) 1); -by (safe_tac (set_cs addSIs [completeness_0])); -by (rtac (weaken_left_insert RS thms.MP) 1); -by (fast_tac (set_cs addSIs [sat_imp]) 1); -by (fast_tac thms_cs 1); -qed "completeness_lemma"; - -val completeness = completeness_lemma RS spec RS mp; - -val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)"; -by (fast_tac (set_cs addSEs [soundness, finite RS completeness]) 1); -qed "thms_iff"; - -writeln"Reached end of file.";