removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
authorclasohm
Tue Dec 13 11:51:12 1994 +0100 (1994-12-13)
changeset 7794ab9176b45b7
parent 778 9a03ed31ea2f
child 780 567f1fe7ea39
removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
src/FOL/FOL.ML
src/FOL/IFOL.ML
     1.1 --- a/src/FOL/FOL.ML	Mon Dec 12 10:26:05 1994 +0100
     1.2 +++ b/src/FOL/FOL.ML	Tue Dec 13 11:51:12 1994 +0100
     1.3 @@ -8,25 +8,10 @@
     1.4  
     1.5  open FOL;
     1.6  
     1.7 -signature FOL_LEMMAS = 
     1.8 -  sig
     1.9 -  val disjCI 		: thm
    1.10 -  val excluded_middle 	: thm
    1.11 -  val excluded_middle_tac: string -> int -> tactic
    1.12 -  val exCI 		: thm
    1.13 -  val ex_classical 	: thm
    1.14 -  val iffCE 		: thm
    1.15 -  val impCE 		: thm
    1.16 -  val notnotD 		: thm
    1.17 -  end;
    1.18 -
    1.19 -
    1.20 -structure FOL_Lemmas : FOL_LEMMAS = 
    1.21 -struct
    1.22  
    1.23  (*** Classical introduction rules for | and EX ***)
    1.24  
    1.25 -val disjCI = prove_goal FOL.thy 
    1.26 +qed_goal "disjCI" FOL.thy 
    1.27     "(~Q ==> P) ==> P|Q"
    1.28   (fn prems=>
    1.29    [ (resolve_tac [classical] 1),
    1.30 @@ -34,14 +19,14 @@
    1.31      (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    1.32  
    1.33  (*introduction rule involving only EX*)
    1.34 -val ex_classical = prove_goal FOL.thy 
    1.35 +qed_goal "ex_classical" FOL.thy 
    1.36     "( ~(EX x. P(x)) ==> P(a)) ==> EX x.P(x)"
    1.37   (fn prems=>
    1.38    [ (resolve_tac [classical] 1),
    1.39      (eresolve_tac (prems RL [exI]) 1) ]);
    1.40  
    1.41  (*version of above, simplifying ~EX to ALL~ *)
    1.42 -val exCI = prove_goal FOL.thy 
    1.43 +qed_goal "exCI" FOL.thy 
    1.44     "(ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)"
    1.45   (fn [prem]=>
    1.46    [ (resolve_tac [ex_classical] 1),
    1.47 @@ -49,7 +34,7 @@
    1.48      (eresolve_tac [notE] 1),
    1.49      (eresolve_tac [exI] 1) ]);
    1.50  
    1.51 -val excluded_middle = prove_goal FOL.thy "~P | P"
    1.52 +qed_goal "excluded_middle" FOL.thy "~P | P"
    1.53   (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    1.54  
    1.55  (*For disjunctive case analysis*)
    1.56 @@ -60,14 +45,14 @@
    1.57  
    1.58  
    1.59  (*Classical implies (-->) elimination. *)
    1.60 -val impCE = prove_goal FOL.thy 
    1.61 +qed_goal "impCE" FOL.thy 
    1.62      "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
    1.63   (fn major::prems=>
    1.64    [ (resolve_tac [excluded_middle RS disjE] 1),
    1.65      (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    1.66  
    1.67  (*Double negation law*)
    1.68 -val notnotD = prove_goal FOL.thy "~~P ==> P"
    1.69 +qed_goal "notnotD" FOL.thy "~~P ==> P"
    1.70   (fn [major]=>
    1.71    [ (resolve_tac [classical] 1), (eresolve_tac [major RS notE] 1) ]);
    1.72  
    1.73 @@ -76,14 +61,9 @@
    1.74  
    1.75  (*Classical <-> elimination.  Proof substitutes P=Q in 
    1.76      ~P ==> ~Q    and    P ==> Q  *)
    1.77 -val iffCE = prove_goalw FOL.thy [iff_def]
    1.78 +qed_goalw "iffCE" FOL.thy [iff_def]
    1.79      "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    1.80   (fn prems =>
    1.81    [ (resolve_tac [conjE] 1),
    1.82      (REPEAT (DEPTH_SOLVE_1 
    1.83  	(etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
    1.84 -
    1.85 -
    1.86 -end;
    1.87 -
    1.88 -open FOL_Lemmas;
     2.1 --- a/src/FOL/IFOL.ML	Mon Dec 12 10:26:05 1994 +0100
     2.2 +++ b/src/FOL/IFOL.ML	Tue Dec 13 11:51:12 1994 +0100
     2.3 @@ -8,88 +8,29 @@
     2.4  
     2.5  open IFOL;
     2.6  
     2.7 -signature IFOL_LEMMAS = 
     2.8 -  sig
     2.9 -  val allE: thm
    2.10 -  val all_cong: thm
    2.11 -  val all_dupE: thm
    2.12 -  val all_impE: thm
    2.13 -  val box_equals: thm
    2.14 -  val conjE: thm
    2.15 -  val conj_cong: thm
    2.16 -  val conj_impE: thm
    2.17 -  val contrapos: thm
    2.18 -  val disj_cong: thm
    2.19 -  val disj_impE: thm
    2.20 -  val eq_cong: thm
    2.21 -  val eq_mp_tac: int -> tactic
    2.22 -  val ex1I: thm
    2.23 -  val ex_ex1I: thm
    2.24 -  val ex1E: thm
    2.25 -  val ex1_equalsE: thm
    2.26 -  val ex1_cong: thm
    2.27 -  val ex_cong: thm
    2.28 -  val ex_impE: thm
    2.29 -  val iffD1: thm
    2.30 -  val iffD2: thm
    2.31 -  val iffE: thm
    2.32 -  val iffI: thm
    2.33 -  val iff_cong: thm
    2.34 -  val iff_impE: thm
    2.35 -  val iff_refl: thm
    2.36 -  val iff_sym: thm
    2.37 -  val iff_trans: thm
    2.38 -  val impE: thm
    2.39 -  val imp_cong: thm
    2.40 -  val imp_impE: thm
    2.41 -  val mp_tac: int -> tactic
    2.42 -  val notE: thm
    2.43 -  val notI: thm
    2.44 -  val not_cong: thm
    2.45 -  val not_impE: thm
    2.46 -  val not_sym: thm
    2.47 -  val not_to_imp: thm
    2.48 -  val pred1_cong: thm
    2.49 -  val pred2_cong: thm
    2.50 -  val pred3_cong: thm
    2.51 -  val pred_congs: thm list
    2.52 -  val rev_mp: thm
    2.53 -  val simp_equals: thm
    2.54 -  val ssubst: thm
    2.55 -  val subst_context: thm
    2.56 -  val subst_context2: thm
    2.57 -  val subst_context3: thm
    2.58 -  val sym: thm
    2.59 -  val trans: thm
    2.60 -  val TrueI: thm
    2.61 -  end;
    2.62  
    2.63 -
    2.64 -structure IFOL_Lemmas : IFOL_LEMMAS =
    2.65 -struct
    2.66 -
    2.67 -val TrueI = prove_goalw IFOL.thy [True_def] "True"
    2.68 +qed_goalw "TrueI" IFOL.thy [True_def] "True"
    2.69   (fn _ => [ (REPEAT (ares_tac [impI] 1)) ]);
    2.70  
    2.71  (*** Sequent-style elimination rules for & --> and ALL ***)
    2.72  
    2.73 -val conjE = prove_goal IFOL.thy 
    2.74 +qed_goal "conjE" IFOL.thy 
    2.75      "[| P&Q; [| P; Q |] ==> R |] ==> R"
    2.76   (fn prems=>
    2.77    [ (REPEAT (resolve_tac prems 1
    2.78        ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN
    2.79                resolve_tac prems 1))) ]);
    2.80  
    2.81 -val impE = prove_goal IFOL.thy 
    2.82 +qed_goal "impE" IFOL.thy 
    2.83      "[| P-->Q;  P;  Q ==> R |] ==> R"
    2.84   (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    2.85  
    2.86 -val allE = prove_goal IFOL.thy 
    2.87 +qed_goal "allE" IFOL.thy 
    2.88      "[| ALL x.P(x); P(x) ==> R |] ==> R"
    2.89   (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    2.90  
    2.91  (*Duplicates the quantifier; for use with eresolve_tac*)
    2.92 -val all_dupE = prove_goal IFOL.thy 
    2.93 +qed_goal "all_dupE" IFOL.thy 
    2.94      "[| ALL x.P(x);  [| P(x); ALL x.P(x) |] ==> R \
    2.95  \    |] ==> R"
    2.96   (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    2.97 @@ -97,16 +38,16 @@
    2.98  
    2.99  (*** Negation rules, which translate between ~P and P-->False ***)
   2.100  
   2.101 -val notI = prove_goalw IFOL.thy [not_def] "(P ==> False) ==> ~P"
   2.102 +qed_goalw "notI" IFOL.thy [not_def] "(P ==> False) ==> ~P"
   2.103   (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
   2.104  
   2.105 -val notE = prove_goalw IFOL.thy [not_def] "[| ~P;  P |] ==> R"
   2.106 +qed_goalw "notE" IFOL.thy [not_def] "[| ~P;  P |] ==> R"
   2.107   (fn prems=>
   2.108    [ (resolve_tac [mp RS FalseE] 1),
   2.109      (REPEAT (resolve_tac prems 1)) ]);
   2.110  
   2.111  (*This is useful with the special implication rules for each kind of P. *)
   2.112 -val not_to_imp = prove_goal IFOL.thy 
   2.113 +qed_goal "not_to_imp" IFOL.thy 
   2.114      "[| ~P;  (P-->False) ==> Q |] ==> Q"
   2.115   (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
   2.116  
   2.117 @@ -115,12 +56,12 @@
   2.118     this implication, then apply impI to move P back into the assumptions.
   2.119     To specify P use something like
   2.120        eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
   2.121 -val rev_mp = prove_goal IFOL.thy "[| P;  P --> Q |] ==> Q"
   2.122 +qed_goal "rev_mp" IFOL.thy "[| P;  P --> Q |] ==> Q"
   2.123   (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
   2.124  
   2.125  
   2.126  (*Contrapositive of an inference rule*)
   2.127 -val contrapos = prove_goal IFOL.thy "[| ~Q;  P==>Q |] ==> ~P"
   2.128 +qed_goal "contrapos" IFOL.thy "[| ~Q;  P==>Q |] ==> ~P"
   2.129   (fn [major,minor]=> 
   2.130    [ (rtac (major RS notE RS notI) 1), 
   2.131      (etac minor 1) ]);
   2.132 @@ -137,34 +78,34 @@
   2.133  
   2.134  (*** If-and-only-if ***)
   2.135  
   2.136 -val iffI = prove_goalw IFOL.thy [iff_def]
   2.137 +qed_goalw "iffI" IFOL.thy [iff_def]
   2.138     "[| P ==> Q;  Q ==> P |] ==> P<->Q"
   2.139   (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
   2.140  
   2.141  
   2.142  (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   2.143 -val iffE = prove_goalw IFOL.thy [iff_def]
   2.144 +qed_goalw "iffE" IFOL.thy [iff_def]
   2.145      "[| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R"
   2.146   (fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]);
   2.147  
   2.148  (* Destruct rules for <-> similar to Modus Ponens *)
   2.149  
   2.150 -val iffD1 = prove_goalw IFOL.thy [iff_def] "[| P <-> Q;  P |] ==> Q"
   2.151 +qed_goalw "iffD1" IFOL.thy [iff_def] "[| P <-> Q;  P |] ==> Q"
   2.152   (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   2.153  
   2.154 -val iffD2 = prove_goalw IFOL.thy [iff_def] "[| P <-> Q;  Q |] ==> P"
   2.155 +qed_goalw "iffD2" IFOL.thy [iff_def] "[| P <-> Q;  Q |] ==> P"
   2.156   (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   2.157  
   2.158 -val iff_refl = prove_goal IFOL.thy "P <-> P"
   2.159 +qed_goal "iff_refl" IFOL.thy "P <-> P"
   2.160   (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]);
   2.161  
   2.162 -val iff_sym = prove_goal IFOL.thy "Q <-> P ==> P <-> Q"
   2.163 +qed_goal "iff_sym" IFOL.thy "Q <-> P ==> P <-> Q"
   2.164   (fn [major] =>
   2.165    [ (rtac (major RS iffE) 1),
   2.166      (rtac iffI 1),
   2.167      (REPEAT (eresolve_tac [asm_rl,mp] 1)) ]);
   2.168  
   2.169 -val iff_trans = prove_goal IFOL.thy
   2.170 +qed_goal "iff_trans" IFOL.thy
   2.171      "!!P Q R. [| P <-> Q;  Q<-> R |] ==> P <-> R"
   2.172   (fn _ =>
   2.173    [ (rtac iffI 1),
   2.174 @@ -177,17 +118,17 @@
   2.175   do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   2.176  ***)
   2.177  
   2.178 -val ex1I = prove_goalw IFOL.thy [ex1_def]
   2.179 +qed_goalw "ex1I" IFOL.thy [ex1_def]
   2.180      "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)"
   2.181   (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
   2.182  
   2.183  (*Sometimes easier to use: the premises have no shared variables*)
   2.184 -val ex_ex1I = prove_goal IFOL.thy
   2.185 +qed_goal "ex_ex1I" IFOL.thy
   2.186      "[| EX x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
   2.187   (fn [ex,eq] => [ (rtac (ex RS exE) 1),
   2.188  		  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
   2.189  
   2.190 -val ex1E = prove_goalw IFOL.thy [ex1_def]
   2.191 +qed_goalw "ex1E" IFOL.thy [ex1_def]
   2.192      "[| EX! x.P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
   2.193   (fn prems =>
   2.194    [ (cut_facts_tac prems 1),
   2.195 @@ -201,7 +142,7 @@
   2.196      resolve_tac (prems RL [iffE]) i THEN
   2.197      REPEAT1 (eresolve_tac [asm_rl,mp] i);
   2.198  
   2.199 -val conj_cong = prove_goal IFOL.thy 
   2.200 +qed_goal "conj_cong" IFOL.thy 
   2.201      "[| P <-> P';  P' ==> Q <-> Q' |] ==> (P&Q) <-> (P'&Q')"
   2.202   (fn prems =>
   2.203    [ (cut_facts_tac prems 1),
   2.204 @@ -209,7 +150,7 @@
   2.205        ORELSE  eresolve_tac [iffE,conjE,mp] 1
   2.206        ORELSE  iff_tac prems 1)) ]);
   2.207  
   2.208 -val disj_cong = prove_goal IFOL.thy 
   2.209 +qed_goal "disj_cong" IFOL.thy 
   2.210      "[| P <-> P';  Q <-> Q' |] ==> (P|Q) <-> (P'|Q')"
   2.211   (fn prems =>
   2.212    [ (cut_facts_tac prems 1),
   2.213 @@ -217,7 +158,7 @@
   2.214        ORELSE  ares_tac [iffI] 1
   2.215        ORELSE  mp_tac 1)) ]);
   2.216  
   2.217 -val imp_cong = prove_goal IFOL.thy 
   2.218 +qed_goal "imp_cong" IFOL.thy 
   2.219      "[| P <-> P';  P' ==> Q <-> Q' |] ==> (P-->Q) <-> (P'-->Q')"
   2.220   (fn prems =>
   2.221    [ (cut_facts_tac prems 1),
   2.222 @@ -225,7 +166,7 @@
   2.223        ORELSE  eresolve_tac [iffE] 1
   2.224        ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
   2.225  
   2.226 -val iff_cong = prove_goal IFOL.thy 
   2.227 +qed_goal "iff_cong" IFOL.thy 
   2.228      "[| P <-> P';  Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
   2.229   (fn prems =>
   2.230    [ (cut_facts_tac prems 1),
   2.231 @@ -233,7 +174,7 @@
   2.232        ORELSE  ares_tac [iffI] 1
   2.233        ORELSE  mp_tac 1)) ]);
   2.234  
   2.235 -val not_cong = prove_goal IFOL.thy 
   2.236 +qed_goal "not_cong" IFOL.thy 
   2.237      "P <-> P' ==> ~P <-> ~P'"
   2.238   (fn prems =>
   2.239    [ (cut_facts_tac prems 1),
   2.240 @@ -241,21 +182,21 @@
   2.241        ORELSE  mp_tac 1
   2.242        ORELSE  eresolve_tac [iffE,notE] 1)) ]);
   2.243  
   2.244 -val all_cong = prove_goal IFOL.thy 
   2.245 +qed_goal "all_cong" IFOL.thy 
   2.246      "(!!x.P(x) <-> Q(x)) ==> (ALL x.P(x)) <-> (ALL x.Q(x))"
   2.247   (fn prems =>
   2.248    [ (REPEAT   (ares_tac [iffI,allI] 1
   2.249        ORELSE   mp_tac 1
   2.250        ORELSE   eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]);
   2.251  
   2.252 -val ex_cong = prove_goal IFOL.thy 
   2.253 +qed_goal "ex_cong" IFOL.thy 
   2.254      "(!!x.P(x) <-> Q(x)) ==> (EX x.P(x)) <-> (EX x.Q(x))"
   2.255   (fn prems =>
   2.256    [ (REPEAT   (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1
   2.257        ORELSE   mp_tac 1
   2.258        ORELSE   iff_tac prems 1)) ]);
   2.259  
   2.260 -val ex1_cong = prove_goal IFOL.thy 
   2.261 +qed_goal "ex1_cong" IFOL.thy 
   2.262      "(!!x.P(x) <-> Q(x)) ==> (EX! x.P(x)) <-> (EX! x.Q(x))"
   2.263   (fn prems =>
   2.264    [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
   2.265 @@ -264,20 +205,20 @@
   2.266  
   2.267  (*** Equality rules ***)
   2.268  
   2.269 -val sym = prove_goal IFOL.thy "a=b ==> b=a"
   2.270 +qed_goal "sym" IFOL.thy "a=b ==> b=a"
   2.271   (fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]);
   2.272  
   2.273 -val trans = prove_goal IFOL.thy "[| a=b;  b=c |] ==> a=c"
   2.274 +qed_goal "trans" IFOL.thy "[| a=b;  b=c |] ==> a=c"
   2.275   (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]);
   2.276  
   2.277  (** ~ b=a ==> ~ a=b **)
   2.278  val [not_sym] = compose(sym,2,contrapos);
   2.279  
   2.280  (*calling "standard" reduces maxidx to 0*)
   2.281 -val ssubst = standard (sym RS subst);
   2.282 +bind_thm ("ssubst", (sym RS subst));
   2.283  
   2.284  (*A special case of ex1E that would otherwise need quantifier expansion*)
   2.285 -val ex1_equalsE = prove_goal IFOL.thy
   2.286 +qed_goal "ex1_equalsE" IFOL.thy
   2.287      "[| EX! x.P(x);  P(a);  P(b) |] ==> a=b"
   2.288   (fn prems =>
   2.289    [ (cut_facts_tac prems 1),
   2.290 @@ -288,18 +229,18 @@
   2.291  
   2.292  (** Polymorphic congruence rules **)
   2.293  
   2.294 -val subst_context = prove_goal IFOL.thy 
   2.295 +qed_goal "subst_context" IFOL.thy 
   2.296     "[| a=b |]  ==>  t(a)=t(b)"
   2.297   (fn prems=>
   2.298    [ (resolve_tac (prems RL [ssubst]) 1),
   2.299      (resolve_tac [refl] 1) ]);
   2.300  
   2.301 -val subst_context2 = prove_goal IFOL.thy 
   2.302 +qed_goal "subst_context2" IFOL.thy 
   2.303     "[| a=b;  c=d |]  ==>  t(a,c)=t(b,d)"
   2.304   (fn prems=>
   2.305    [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   2.306  
   2.307 -val subst_context3 = prove_goal IFOL.thy 
   2.308 +qed_goal "subst_context3" IFOL.thy 
   2.309     "[| a=b;  c=d;  e=f |]  ==>  t(a,c,e)=t(b,d,f)"
   2.310   (fn prems=>
   2.311    [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   2.312 @@ -308,7 +249,7 @@
   2.313  	a = b
   2.314  	|   |
   2.315  	c = d	*)
   2.316 -val box_equals = prove_goal IFOL.thy
   2.317 +qed_goal "box_equals" IFOL.thy
   2.318      "[| a=b;  a=c;  b=d |] ==> c=d"  
   2.319   (fn prems=>
   2.320    [ (resolve_tac [trans] 1),
   2.321 @@ -317,7 +258,7 @@
   2.322      (REPEAT (resolve_tac prems 1)) ]);
   2.323  
   2.324  (*Dual of box_equals: for proving equalities backwards*)
   2.325 -val simp_equals = prove_goal IFOL.thy
   2.326 +qed_goal "simp_equals" IFOL.thy
   2.327      "[| a=c;  b=d;  c=d |] ==> a=b"  
   2.328   (fn prems=>
   2.329    [ (resolve_tac [trans] 1),
   2.330 @@ -326,21 +267,21 @@
   2.331  
   2.332  (** Congruence rules for predicate letters **)
   2.333  
   2.334 -val pred1_cong = prove_goal IFOL.thy
   2.335 +qed_goal "pred1_cong" IFOL.thy
   2.336      "a=a' ==> P(a) <-> P(a')"
   2.337   (fn prems =>
   2.338    [ (cut_facts_tac prems 1),
   2.339      (rtac iffI 1),
   2.340      (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   2.341  
   2.342 -val pred2_cong = prove_goal IFOL.thy
   2.343 +qed_goal "pred2_cong" IFOL.thy
   2.344      "[| a=a';  b=b' |] ==> P(a,b) <-> P(a',b')"
   2.345   (fn prems =>
   2.346    [ (cut_facts_tac prems 1),
   2.347      (rtac iffI 1),
   2.348      (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   2.349  
   2.350 -val pred3_cong = prove_goal IFOL.thy
   2.351 +qed_goal "pred3_cong" IFOL.thy
   2.352      "[| a=a';  b=b';  c=c' |] ==> P(a,b,c) <-> P(a',b',c')"
   2.353   (fn prems =>
   2.354    [ (cut_facts_tac prems 1),
   2.355 @@ -366,50 +307,45 @@
   2.356     R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   2.357      (preprint, University of St Andrews, 1991)  ***)
   2.358  
   2.359 -val conj_impE = prove_goal IFOL.thy 
   2.360 +qed_goal "conj_impE" IFOL.thy 
   2.361      "[| (P&Q)-->S;  P-->(Q-->S) ==> R |] ==> R"
   2.362   (fn major::prems=>
   2.363    [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
   2.364  
   2.365 -val disj_impE = prove_goal IFOL.thy 
   2.366 +qed_goal "disj_impE" IFOL.thy 
   2.367      "[| (P|Q)-->S;  [| P-->S; Q-->S |] ==> R |] ==> R"
   2.368   (fn major::prems=>
   2.369    [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]);
   2.370  
   2.371  (*Simplifies the implication.  Classical version is stronger. 
   2.372    Still UNSAFE since Q must be provable -- backtracking needed.  *)
   2.373 -val imp_impE = prove_goal IFOL.thy 
   2.374 +qed_goal "imp_impE" IFOL.thy 
   2.375      "[| (P-->Q)-->S;  [| P; Q-->S |] ==> Q;  S ==> R |] ==> R"
   2.376   (fn major::prems=>
   2.377    [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
   2.378  
   2.379  (*Simplifies the implication.  Classical version is stronger. 
   2.380    Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   2.381 -val not_impE = prove_goal IFOL.thy
   2.382 +qed_goal "not_impE" IFOL.thy
   2.383      "[| ~P --> S;  P ==> False;  S ==> R |] ==> R"
   2.384   (fn major::prems=>
   2.385    [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
   2.386  
   2.387  (*Simplifies the implication.   UNSAFE.  *)
   2.388 -val iff_impE = prove_goal IFOL.thy 
   2.389 +qed_goal "iff_impE" IFOL.thy 
   2.390      "[| (P<->Q)-->S;  [| P; Q-->S |] ==> Q;  [| Q; P-->S |] ==> P;  \
   2.391  \       S ==> R |] ==> R"
   2.392   (fn major::prems=>
   2.393    [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
   2.394  
   2.395  (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   2.396 -val all_impE = prove_goal IFOL.thy 
   2.397 +qed_goal "all_impE" IFOL.thy 
   2.398      "[| (ALL x.P(x))-->S;  !!x.P(x);  S ==> R |] ==> R"
   2.399   (fn major::prems=>
   2.400    [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
   2.401  
   2.402  (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   2.403 -val ex_impE = prove_goal IFOL.thy 
   2.404 +qed_goal "ex_impE" IFOL.thy 
   2.405      "[| (EX x.P(x))-->S;  P(x)-->S ==> R |] ==> R"
   2.406   (fn major::prems=>
   2.407    [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
   2.408 -
   2.409 -end;
   2.410 -
   2.411 -open IFOL_Lemmas;
   2.412 -