# HG changeset patch
# User lcp
# Date 775490842 -7200
# Node ID 9c724f7085f9ea4d3a5f1d31737988bb0ad6166a
# Parent  0842a38074e72d00e29465ea2be91967402898d3
ZF/ex/PropLog/sat_XXX: renamed logcon_XXX, since the relation is logical
consequence rather than satisfaction

diff -r 0842a38074e7 -r 9c724f7085f9 src/ZF/ex/PropLog.ML
--- a/src/ZF/ex/PropLog.ML	Fri Jul 29 15:32:17 1994 +0200
+++ b/src/ZF/ex/PropLog.ML	Fri Jul 29 16:07:22 1994 +0200
@@ -158,7 +158,7 @@
 val thms_notE = standard (thms_MP RS thms_FlsE);
 
 (*Soundness of the rules wrt truth-table semantics*)
-goalw PropThms.thy [sat_def] "!!H. H |- p ==> H |= p";
+goalw PropThms.thy [logcon_def] "!!H. H |- p ==> H |= p";
 by (etac PropThms.induct 1);
 by (fast_tac (ZF_cs addSDs [is_true_Imp RS iffD1 RS mp]) 5);
 by (ALLGOALS (asm_simp_tac prop_ss));
@@ -198,12 +198,12 @@
 val hyps_thms_if = result();
 
 (*Key lemma for completeness; yields a set of assumptions satisfying p*)
-val [premp,sat] = goalw PropThms.thy [sat_def]
+val [premp,sat] = goalw PropThms.thy [logcon_def]
     "[| p: prop;  0 |= p |] ==> hyps(p,t) |- p";
 by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
     rtac (premp RS hyps_thms_if) 2);
 by (fast_tac ZF_cs 1);
-val sat_thms_p = result();
+val logcon_thms_p = result();
 
 (*For proving certain theorems in our new propositional logic*)
 val thms_cs = 
@@ -278,7 +278,7 @@
 val [premp,sat] = goal PropThms.thy
     "[| p: prop;  0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
 by (rtac (premp RS hyps_finite RS Fin_induct) 1);
-by (simp_tac (prop_ss addsimps [premp, sat, sat_thms_p, Diff_0]) 1);
+by (simp_tac (prop_ss addsimps [premp, sat, logcon_thms_p, Diff_0]) 1);
 by (safe_tac ZF_cs);
 (*Case hyps(p,t)-cons(#v,Y) |- p *)
 by (rtac thms_excluded_middle_rule 1);
@@ -305,16 +305,16 @@
 val completeness_0 = result();
 
 (*A semantic analogue of the Deduction Theorem*)
-goalw PropThms.thy [sat_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
+goalw PropThms.thy [logcon_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
 by (simp_tac prop_ss 1);
 by (fast_tac ZF_cs 1);
-val sat_Imp = result();
+val logcon_Imp = result();
 
 goal PropThms.thy "!!H. H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p";
 by (etac Fin_induct 1);
 by (safe_tac (ZF_cs addSIs [completeness_0]));
 by (rtac (weaken_left_cons RS thms_MP) 1);
-by (fast_tac (ZF_cs addSIs [sat_Imp,ImpI]) 1);
+by (fast_tac (ZF_cs addSIs [logcon_Imp,ImpI]) 1);
 by (fast_tac thms_cs 1);
 val completeness_lemma = result();
 
diff -r 0842a38074e7 -r 9c724f7085f9 src/ZF/ex/PropLog.thy
--- a/src/ZF/ex/PropLog.thy	Fri Jul 29 15:32:17 1994 +0200
+++ b/src/ZF/ex/PropLog.thy	Fri Jul 29 16:07:22 1994 +0200
@@ -32,8 +32,9 @@
    "is_true(p,t) == prop_rec(p, 0,  %v. if(v:t, 1, 0), \
 \                               %p q tp tq. if(tp=1,tq,1))         =  1"
 
-  (*For every valuation, if all elements of H are true then so is p*)
-  sat_def     "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)"
+  (*Logical consequence: for every valuation, if all elements of H are true
+     then so is p*)
+  logcon_def  "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)"
 
   (** A finite set of hypotheses from t and the Vars in p **)
   hyps_def