ex/PL.ML

Initial revision

(*  Title: 	HOL/ex/prop-log.ML
    ID:         $Id$
    Author: 	Tobias Nipkow & Lawrence C Paulson
    Copyright   1993  TU Muenchen & University of Cambridge

For ex/prop-log.thy.  Inductive definition of propositional logic.
Soundness and completeness w.r.t. truth-tables.

Prove: If H|=p then G|=p where G:Fin(H)
*)

open PL;

val rule_defs = [axK_def, axS_def, axDN_def, ruleMP_def];


(** Monotonicity and unfolding of the function **)

goalw PL.thy rule_defs "mono(%X. H Un axK Un axS Un axDN Un ruleMP(X))";
by (rtac monoI 1);
by(fast_tac set_cs 1);
val thms_bnd_mono = result();

goalw PL.thy [thms_def] "!!G H. G<=H ==> thms(G) <= thms(H)";
by (REPEAT (ares_tac [subset_refl, Un_mono, lfp_mono] 1));
val thms_mono = result();

(** Introduction rules for the consequence relation **)

(* thms(H) = H Int Un axK Un axS Un ruleMP(thms(H)) *)
val thms_unfold = thms_bnd_mono RS (thms_def RS def_lfp_Tarski);

(*Proof by hypothesis*)
val prems = goalw PL.thy [conseq_def]  "p:H ==> H |- p";
by (rtac (thms_unfold RS ssubst) 1);
by (fast_tac (set_cs addSIs prems) 1);
val conseq_H = result();

(*Proof by axiom K*)
goalw PL.thy [conseq_def] "H |- p->q->p";
by (rtac (thms_unfold RS ssubst) 1);
by (rewtac axK_def);
by (fast_tac set_cs  1);
val conseq_K = result();

(*Proof by axiom S*)
goalw PL.thy [conseq_def] "H |- (p->q->r) -> (p->q) -> p -> r";
by (rtac (thms_unfold RS ssubst) 1);
by (rewtac axS_def);
by (fast_tac set_cs  1);
val conseq_S = result();

(*Proof by axiom DN (double negation) *)
goalw PL.thy [conseq_def]  "H |- ((p->false) -> false) -> p";
by (rtac (thms_unfold RS ssubst) 1);
by (rewtac axDN_def);
by (fast_tac set_cs  1);
val conseq_DN = result();

(*Proof by rule MP (Modus Ponens) *)
val [prempq,premp] = goalw PL.thy [conseq_def]
    "[| H |- p->q;  H |- p |] ==> H |- q";
by (rtac (thms_unfold RS ssubst) 1);
by (rewtac ruleMP_def);
by (fast_tac (set_cs addSIs [premp,prempq]) 1);
val conseq_MP = result();

(*Rule is called I for Identity Combinator, not for Introduction*)
goal PL.thy "H |- p->p";
by (rtac (conseq_S RS conseq_MP RS conseq_MP) 1);
by (rtac conseq_K 2);
by (rtac conseq_K 1);
val conseq_I = result();

(** Weakening, left and right **)

(*This order of premises is convenient with RS*)
val prems = goalw PL.thy [conseq_def] "[| G<=H;  G |- p |] ==> H |- p";
by (rtac (thms_mono RS subsetD) 1);
by (REPEAT (resolve_tac prems 1));
val weaken_left = result();

(* 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;

val prems = goal PL.thy "H |- q ==> H |- p->q";
by (rtac (conseq_K RS conseq_MP) 1);
by (REPEAT (resolve_tac prems 1));
val weaken_right = result();

(** Rule induction for H|-p **)

(*Careful unfolding/folding to avoid a big expansion*)
val major::prems = goalw PL.thy [conseq_def]
  "[| H |- a;							\
\     !!x. x:H ==> P(x);				\
\     !!x y. P(x->y->x);			\
\     !!x y z. P((x->y->z)->(x->y)->x->z);			\
\     !!x. P(((x->false)->false)->x);			\
\     !!x y. [| H |- x->y;  H |- x;  P(x->y);  P(x) |] ==> P(y) \
\  |] ==> P(a)";
by (rtac (major RS (thms_def RS def_induct)) 1);
by (rtac thms_bnd_mono 1);
by (rewrite_tac rule_defs);
by (fast_tac (set_cs addIs prems) 1);
val conseq_induct = result();

(*The deduction theorem*)
val [major] = goal PL.thy "insert(p,H) |- q  ==>  H |- p->q";
by (rtac (major RS conseq_induct) 1);
by (fast_tac (set_cs addIs [conseq_I, conseq_H RS weaken_right]) 1);
by (fast_tac (set_cs addIs [conseq_K RS weaken_right]) 1);
by (fast_tac (set_cs addIs [conseq_S RS weaken_right]) 1);
by (fast_tac (set_cs addIs [conseq_DN RS weaken_right]) 1);
by (fast_tac (set_cs addIs [conseq_S RS conseq_MP RS conseq_MP]) 1);
val deduction = result();


(*The cut rule*)
val prems = goal PL.thy "[| H|-p;  insert(p,H) |- q |] ==>  H |- q";
by (rtac (deduction RS conseq_MP) 1);
by (REPEAT (resolve_tac prems 1));
val cut = result();

val prems = goal PL.thy "H |- false ==> H |- p";
by (rtac (conseq_DN RS conseq_MP) 1);
by (rtac weaken_right 1);
by (resolve_tac prems 1);
val conseq_falseE = result();

(* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
val conseq_notE = standard (conseq_MP RS conseq_falseE);

(** The function eval **)

val pl_ss = set_ss addsimps [pl_rec_var,pl_rec_false,pl_rec_imp];

goalw PL.thy [eval_def] "tt[false] = False";
by (simp_tac pl_ss 1);
val eval_false = result();

goalw PL.thy [eval_def] "tt[#v] = (v:tt)";
by (simp_tac pl_ss 1);
val eval_var = result();

goalw PL.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
by (simp_tac pl_ss 1);
val eval_imp = result();

val pl_ss = pl_ss addsimps [eval_false, eval_var, eval_imp];

(** The function hyps **)

goalw PL.thy [hyps_def] "hyps(false,tt) = {}";
by (simp_tac pl_ss 1);
val hyps_false = result();

goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, #v->false)}";
by (simp_tac pl_ss 1);
val hyps_var = result();

goalw PL.thy [hyps_def] "hyps(p->q,tt) = hyps(p,tt) Un hyps(q,tt)";
by (simp_tac pl_ss 1);
val hyps_imp = result();

val pl_ss = pl_ss addsimps [hyps_false, hyps_var, hyps_imp];

val ball_eq = prove_goalw Set.thy [Ball_def] "(!x:A.P(x)) = (!x.x:A --> P(x))"
	(fn _ => [rtac refl 1]);

(*Soundness of the rules wrt truth-table semantics*)
val [major] = goalw PL.thy [sat_def] "H |- p ==> H |= p";
by (rtac (major RS conseq_induct) 1);
by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5);
by (ALLGOALS (asm_simp_tac(pl_ss addsimps
                [ball_eq,not_def RS fun_cong RS sym])));
val soundness = result();

(** Structural induction on pl

val major::prems = goalw PL.thy pl_defs
  "[| q: pl;  				\
\     P(false);				\
\     !!v. v:nat ==> P(#v);        \
\     !!q1 q2. [| q1: pl;  q2: pl;  P(q1);  P(q2) |] ==> P(q1->q2) \
\  |] ==> P(q)";
by (rtac (major RS sexp_induct) 1);
by (etac nat_induct 1);
by (REPEAT (ares_tac prems 1));
val pl_induct = result();
 **)
(*** Towards the completeness proof ***)

val [premf] = goal PL.thy "H |- p->false ==> H |- p->q";
by (rtac deduction 1);
by (rtac (premf RS weaken_left_insert RS conseq_notE) 1);
by (rtac conseq_H 1);
by (rtac insertI1 1);
val false_imp = result();

val [premp,premq] = goal PL.thy
    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false";
by (rtac deduction 1);
by (rtac (premq RS weaken_left_insert RS conseq_MP) 1);
by (rtac (conseq_H RS conseq_MP) 1);
by (rtac insertI1 1);
by (rtac (premp RS weaken_left_insert) 1);
val imp_false = result();

(*This formulation is required for strong induction hypotheses*)
goal PL.thy "hyps(p,tt) |- if(tt[p], p, p->false)";
by (rtac (expand_if RS iffD2) 1);
by(res_inst_tac[("x","p")]spec 1);
by (rtac pl_ind 1);
by (ALLGOALS (simp_tac (pl_ss addsimps [conseq_I, conseq_H])));
by (fast_tac (set_cs addIs [weaken_left_Un1, weaken_left_Un2, 
			   weaken_right, imp_false]
                    addSEs [false_imp]) 1);
val hyps_conseq_if = result();

(*Key lemma for completeness; yields a set of assumptions satisfying p*)
val [sat] = goalw PL.thy [sat_def] "{} |= p ==> hyps(p,tt) |- p";
by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
    rtac hyps_conseq_if 2);
by (fast_tac set_cs 1);
val sat_conseq_p = result();

(*For proving certain theorems in our new propositional logic*)
val conseq_cs = 
    set_cs addSIs [deduction] addIs [conseq_H, conseq_H RS conseq_MP];

(*The excluded middle in the form of an elimination rule*)
goal PL.thy "H |- (p->q) -> ((p->false)->q) -> q";
by (rtac (deduction RS deduction) 1);
by (rtac (conseq_DN RS conseq_MP) 1);
by (ALLGOALS (best_tac (conseq_cs addSIs prems)));
val conseq_excluded_middle = result();

(*Hard to prove directly because it requires cuts*)
val prems = goal PL.thy
    "[| insert(p,H) |- q;  insert(p->false,H) |- q |] ==> H |- q";
by (rtac (conseq_excluded_middle RS conseq_MP RS conseq_MP) 1);
by (REPEAT (resolve_tac (prems@[deduction]) 1));
val conseq_excluded_middle_rule = result();

(*** 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 PL.thy "!p.hyps(p, t-{v}) <= insert(#v->false, hyps(p,t)-{#v})";
by (rtac pl_ind 1);
by (simp_tac pl_ss 1);
by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
by (fast_tac (set_cs addSEs [sym RS var_neq_imp] addSDs [var_inject]) 1);
by (simp_tac pl_ss 1);
by (fast_tac set_cs 1);
val hyps_Diff = result() RS spec;

(*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 PL.thy "!p.hyps(p, insert(v,t)) <= insert(#v, hyps(p,t)-{#v->false})";
by (rtac pl_ind 1);
by (simp_tac pl_ss 1);
by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1);
by (fast_tac (set_cs addSEs [var_neq_imp, imp_inject] addSDs [var_inject]) 1);
by (simp_tac pl_ss 1);
by (fast_tac set_cs 1);
val hyps_insert = result() RS spec;

(** Two lemmas for use with weaken_left **)

goal Set.thy "B-C <= insert(a, B-insert(a,C))";
by (fast_tac set_cs 1);
val insert_Diff_same = result();

goal Set.thy "insert(a, B-{c}) - D <= insert(a, B-insert(c,D))";
by (fast_tac set_cs 1);
val insert_Diff_subset2 = result();

(*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 PL.thy "!p.hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})";
by (rtac pl_ind 1);
by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN'
              fast_tac (set_cs addSIs [Fin_0I, Fin_insertI, Fin_UnI])));
val hyps_finite = result() RS spec;

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 PL.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_conseq_p]) 1);
by (safe_tac set_cs);
(*Case hyps(p,t)-insert(#v,Y) |- p *)
by (rtac conseq_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 conseq_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);
val completeness_0_lemma = result();

(*The base case for completeness*)
val [sat] = goal PL.thy "{} |= p ==> {} |- p";
by (rtac (Diff_cancel RS subst) 1);
by (rtac (sat RS (completeness_0_lemma RS spec)) 1);
val completeness_0 = result();

(*A semantic analogue of the Deduction Theorem*)
val [sat] = goalw PL.thy [sat_def] "insert(p,H) |= q ==> H |= p->q";
by (simp_tac pl_ss 1);
by (cfast_tac [sat] 1);
val sat_imp = result();

val [finite] = goal PL.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 conseq_MP) 1);
by (fast_tac (set_cs addSIs [sat_imp]) 1);
by (fast_tac conseq_cs 1);
val completeness_lemma = result();

val completeness = completeness_lemma RS spec RS mp;

val [finite] = goal PL.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
by (fast_tac (set_cs addSEs [soundness, finite RS completeness]) 1);
val conseq_iff = result();

writeln"Reached end of file.";