Updated PL to PropLog using Larrys ind. defs.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/PropLog.ML	Tue Aug 30 10:05:46 1994 +0200
@@ -0,0 +1,234 @@
+(*  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.";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/PropLog.thy	Tue Aug 30 10:05:46 1994 +0200
@@ -0,0 +1,61 @@
+(*  Title: 	HOL/ex/pl.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow
+    Copyright   1994  TU Muenchen
+
+Inductive definition of propositional logic.
+*)
+
+PropLog = Finite +
+datatype
+    'a pl = false | var ('a) ("#_" [1000]) | "->" ('a pl,'a pl) (infixr 90)
+consts
+  thms :: "'a pl set => 'a pl set"
+  "|-" 	:: "['a pl set, 'a pl] => bool"	(infixl 50)
+  "|="	:: "['a pl set, 'a pl] => bool"	(infixl 50)
+  eval2	:: "['a pl, 'a set] => bool"
+  eval	:: "['a set, 'a pl] => bool"	("_[_]" [100,0] 100)
+  hyps	:: "['a pl, 'a set] => 'a pl set"
+
+translations
+  "H |- p" == "p : thms(H)"
+
+inductive "thms(H)"
+  intrs
+  H   "p:H ==> H |- p"
+  K   "H |- p->q->p"
+  S   "H |- (p->q->r) -> (p->q) -> p->r"
+  DN  "H |- ((p->false) -> false) -> p"
+  MP  "[| H |- p->q; H |- p |] ==> H |- q"
+
+rules
+
+  (** Proof theory for propositional logic
+
+  axK_def   "axK ==  {x . ? p q.   x = p->q->p}"
+  axS_def   "axS ==  {x . ? p q r. x = (p->q->r) -> (p->q) -> p->r}"
+  axDN_def  "axDN == {x . ? p.     x = ((p->false) -> false) -> p}"
+
+  (*the use of subsets simplifies the proof of monotonicity*)
+  ruleMP_def  "ruleMP(X) == {q. ? p:X. p->q : X}"
+
+  thms_def
+   "thms(H) == lfp(%X. H Un axK Un axS Un axDN Un ruleMP(X))"
+  
+  conseq_def  "H |- p == p : thms(H)"
+**)
+  sat_def "H |= p  ==  (!tt. (!q:H. tt[q]) --> tt[p])"
+
+  eval_def "tt[p] == eval2(p,tt)"
+
+primrec eval2 pl
+  eval2_false "eval2(false) = (%x.False)"
+  eval2_var   "eval2(#v) = (%tt.v:tt)"
+  eval2_imp   "eval2(p->q) = (%tt.eval2(p,tt)-->eval2(q,tt))"
+
+primrec hyps pl
+  hyps_false "hyps(false) = (%tt.{})"
+  hyps_var   "hyps(#v) = (%tt.{if(v:tt, #v, #v->false)})"
+  hyps_imp   "hyps(p->q) = (%tt.hyps(p,tt) Un hyps(q,tt))"
+
+end

--- a/ex/ROOT.ML	Tue Aug 30 10:04:49 1994 +0200
+++ b/ex/ROOT.ML	Tue Aug 30 10:05:46 1994 +0200
@@ -21,7 +21,7 @@
 time_use_thy "NatSum";
 time_use     "ex/set.ML";
 time_use_thy "Acc";
-time_use_thy "PL";
+time_use_thy "PropLog";
 time_use_thy "Term";
 time_use_thy "Simult";
 time_use_thy "MT";