src/ZF/Bool.ML
changeset 760 f0200e91b272
parent 129 dc50a4b96d7b
child 1461 6bcb44e4d6e5
--- a/src/ZF/Bool.ML	Wed Dec 07 12:34:47 1994 +0100
+++ b/src/ZF/Bool.ML	Wed Dec 07 13:12:04 1994 +0100
@@ -14,15 +14,15 @@
 
 goalw Bool.thy bool_defs "1 : bool";
 by (rtac (consI1 RS consI2) 1);
-val bool_1I = result();
+qed "bool_1I";
 
 goalw Bool.thy bool_defs "0 : bool";
 by (rtac consI1 1);
-val bool_0I = result();
+qed "bool_0I";
 
 goalw Bool.thy bool_defs "1~=0";
 by (rtac succ_not_0 1);
-val one_not_0 = result();
+qed "one_not_0";
 
 (** 1=0 ==> R **)
 val one_neq_0 = one_not_0 RS notE;
@@ -31,36 +31,36 @@
     "[| c: bool;  c=1 ==> P;  c=0 ==> P |] ==> P";
 by (rtac (major RS consE) 1);
 by (REPEAT (eresolve_tac (singletonE::prems) 1));
-val boolE = result();
+qed "boolE";
 
 (** cond **)
 
 (*1 means true*)
 goalw Bool.thy bool_defs "cond(1,c,d) = c";
 by (rtac (refl RS if_P) 1);
-val cond_1 = result();
+qed "cond_1";
 
 (*0 means false*)
 goalw Bool.thy bool_defs "cond(0,c,d) = d";
 by (rtac (succ_not_0 RS not_sym RS if_not_P) 1);
-val cond_0 = result();
+qed "cond_0";
 
 val major::prems = goal Bool.thy 
     "[|  b: bool;  c: A(1);  d: A(0) |] ==> cond(b,c,d): A(b)";
 by (rtac (major RS boolE) 1);
 by (asm_simp_tac (ZF_ss addsimps (cond_1::prems)) 1);
 by (asm_simp_tac (ZF_ss addsimps (cond_0::prems)) 1);
-val cond_type = result();
+qed "cond_type";
 
 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(1) = c";
 by (rewtac rew);
 by (rtac cond_1 1);
-val def_cond_1 = result();
+qed "def_cond_1";
 
 val [rew] = goal Bool.thy "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d";
 by (rewtac rew);
 by (rtac cond_0 1);
-val def_cond_0 = result();
+qed "def_cond_0";
 
 fun conds def = [standard (def RS def_cond_1), standard (def RS def_cond_0)];
 
@@ -72,19 +72,19 @@
 
 val [xor_1,xor_0] = conds xor_def;
 
-val not_type = prove_goalw Bool.thy [not_def]
+qed_goalw "not_type" Bool.thy [not_def]
     "a:bool ==> not(a) : bool"
  (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
 
-val and_type = prove_goalw Bool.thy [and_def]
+qed_goalw "and_type" Bool.thy [and_def]
     "[| a:bool;  b:bool |] ==> a and b : bool"
  (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
 
-val or_type = prove_goalw Bool.thy [or_def]
+qed_goalw "or_type" Bool.thy [or_def]
     "[| a:bool;  b:bool |] ==> a or b : bool"
  (fn prems=> [ (typechk_tac (prems@[bool_1I, bool_0I, cond_type])) ]);
 
-val xor_type = prove_goalw Bool.thy [xor_def]
+qed_goalw "xor_type" Bool.thy [xor_def]
     "[| a:bool;  b:bool |] ==> a xor b : bool"
  (fn prems=> [ (typechk_tac(prems@[bool_1I, bool_0I, cond_type, not_type])) ]);
 
@@ -102,58 +102,58 @@
 
 goal Bool.thy "!!a. a:bool ==> not(not(a)) = a";
 by (bool0_tac 1);
-val not_not = result();
+qed "not_not";
 
 goal Bool.thy "!!a b. a:bool ==> not(a and b) = not(a) or not(b)";
 by (bool0_tac 1);
-val not_and = result();
+qed "not_and";
 
 goal Bool.thy "!!a b. a:bool ==> not(a or b) = not(a) and not(b)";
 by (bool0_tac 1);
-val not_or = result();
+qed "not_or";
 
 (*** Laws about 'and' ***)
 
 goal Bool.thy "!!a. a: bool ==> a and a = a";
 by (bool0_tac 1);
-val and_absorb = result();
+qed "and_absorb";
 
 goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a and b = b and a";
 by (etac boolE 1);
 by (bool0_tac 1);
 by (bool0_tac 1);
-val and_commute = result();
+qed "and_commute";
 
 goal Bool.thy
  "!!a. a: bool ==> (a and b) and c  =  a and (b and c)";
 by (bool0_tac 1);
-val and_assoc = result();
+qed "and_assoc";
 
 goal Bool.thy
  "!!a. [| a: bool; b:bool; c:bool |] ==> \
 \      (a or b) and c  =  (a and c) or (b and c)";
 by (REPEAT (bool0_tac 1));
-val and_or_distrib = result();
+qed "and_or_distrib";
 
 (** binary orion **)
 
 goal Bool.thy "!!a. a: bool ==> a or a = a";
 by (bool0_tac 1);
-val or_absorb = result();
+qed "or_absorb";
 
 goal Bool.thy "!!a b. [| a: bool; b:bool |] ==> a or b = b or a";
 by (etac boolE 1);
 by (bool0_tac 1);
 by (bool0_tac 1);
-val or_commute = result();
+qed "or_commute";
 
 goal Bool.thy "!!a. a: bool ==> (a or b) or c  =  a or (b or c)";
 by (bool0_tac 1);
-val or_assoc = result();
+qed "or_assoc";
 
 goal Bool.thy
  "!!a b c. [| a: bool; b: bool; c: bool |] ==> \
 \          (a and b) or c  =  (a or c) and (b or c)";
 by (REPEAT (bool0_tac 1));
-val or_and_distrib = result();
+qed "or_and_distrib";