ex/PropLog.ML

--- a/ex/PropLog.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/PropLog.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -14,12 +14,12 @@
 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();
+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);
-val thms_I = result();
+qed "thms_I";
 
 (** Weakening, left and right **)
 
@@ -36,7 +36,7 @@
 
 goal PropLog.thy "!!H. H |- q ==> H |- p->q";
 by(fast_tac (HOL_cs addIs [thms.K,thms.MP]) 1);
-val weaken_right = result();
+qed "weaken_right";
 
 (*The deduction theorem*)
 goal PropLog.thy "!!H. insert(p,H) |- q  ==>  H |- p->q";
@@ -46,7 +46,7 @@
 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();
+qed "deduction";
 
 
 (* "[| insert(p,H) |- q; H |- p |] ==> H |- q"
@@ -68,15 +68,15 @@
 
 goalw PropLog.thy [eval_def] "tt[false] = False";
 by (simp_tac pl_ss 1);
-val eval_false = result();
+qed "eval_false";
 
 goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)";
 by (simp_tac pl_ss 1);
-val eval_var = result();
+qed "eval_var";
 
 goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
 by (simp_tac pl_ss 1);
-val eval_imp = result();
+qed "eval_imp";
 
 val pl_ss = pl_ss addsimps [eval_false, eval_var, eval_imp];
 
@@ -85,7 +85,7 @@
 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();
+qed "soundness";
 
 (*** Towards the completeness proof ***)
 
@@ -94,7 +94,7 @@
 by (etac (weaken_left_insert RS thms_notE) 1);
 by (rtac thms.H 1);
 by (rtac insertI1 1);
-val false_imp = result();
+qed "false_imp";
 
 val [premp,premq] = goal PropLog.thy
     "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false";
@@ -103,7 +103,7 @@
 by (rtac (thms.H RS thms.MP) 1);
 by (rtac insertI1 1);
 by (rtac (premp RS weaken_left_insert) 1);
-val imp_false = result();
+qed "imp_false";
 
 (*This formulation is required for strong induction hypotheses*)
 goal PropLog.thy "hyps(p,tt) |- if(tt[p], p, p->false)";
@@ -113,14 +113,14 @@
 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();
+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);
-val sat_thms_p = result();
+qed "sat_thms_p";
 
 (*For proving certain theorems in our new propositional logic*)
 val thms_cs = 
@@ -131,14 +131,14 @@
 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();
+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));
-val thms_excluded_middle_rule = result();
+qed "thms_excluded_middle_rule";
 
 (*** Completeness -- lemmas for reducing the set of assumptions ***)
 
@@ -150,7 +150,7 @@
 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();
+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)) *)
@@ -160,17 +160,17 @@
 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();
+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);
-val insert_Diff_same = result();
+qed "insert_Diff_same";
 
 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();
+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))*)
@@ -178,7 +178,7 @@
 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();
+qed "hyps_finite";
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
 
@@ -203,19 +203,19 @@
 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();
+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);
-val completeness_0 = result();
+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);
-val sat_imp = result();
+qed "sat_imp";
 
 val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
 by (rtac (finite RS Fin_induct) 1);
@@ -223,12 +223,12 @@
 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();
+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);
-val thms_iff = result();
+qed "thms_iff";
 
 writeln"Reached end of file.";