diff -r 000000000000 -r 7949f97df77a ex/PL.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/PL.ML	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,344 @@
+(*  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.";
+
+