ex/PropLog.ML

added IOA to isabelle/HOL

(*  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));
val thms_mono = result();

(*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);
val thms_I = result();

(** Weakening, left and right **)

(* "[| G<=H;  G |- p |] ==> H |- p"
   This order of premises is convenient with RS
*)
val weaken_left = standard (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);
val weaken_right = result();

(*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);
val deduction = result();


(* "[| 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 *)
val thms_notE = standard (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);
val eval_false = result();

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

goalw PropLog.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];

(*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));
val soundness = result();

(*** 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);
val false_imp = result();

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);
val imp_false = result();

(*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);
val hyps_thms_if = result();

(*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);
val sat_thms_p = result();

(*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)));
val thms_excluded_middle = result();

(*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));
val thms_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 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);
val hyps_Diff = result();

(*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);
val hyps_insert = result();

(** 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 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])));
val hyps_finite = result();

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);
val completeness_0_lemma = result();

(*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);
val completeness_0 = result();

(*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);
val sat_imp = result();

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);
val completeness_lemma = result();

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);
val thms_iff = result();

writeln"Reached end of file.";