converted to Isar theory format;
authorwenzelm
Sun Sep 18 14:25:48 2005 +0200 (2005-09-18)
changeset 17480fd19f77dcf60
parent 17479 68a7acb5f22e
child 17481 75166ebb619b
converted to Isar theory format;
src/FOLP/FOLP.ML
src/FOLP/FOLP.thy
src/FOLP/FOLP_lemmas.ML
src/FOLP/IFOLP.ML
src/FOLP/IFOLP.thy
src/FOLP/IsaMakefile
src/FOLP/ROOT.ML
src/FOLP/ex/If.ML
src/FOLP/ex/If.thy
src/FOLP/ex/Nat.ML
src/FOLP/ex/Nat.thy
src/FOLP/ex/ROOT.ML
src/FOLP/ex/cla.ML
src/FOLP/ex/foundn.ML
src/FOLP/ex/int.ML
src/FOLP/ex/intro.ML
src/FOLP/ex/prop.ML
src/FOLP/ex/quant.ML
src/FOLP/simpdata.ML
     1.1 --- a/src/FOLP/FOLP.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,76 +0,0 @@
     1.4 -(*  Title:      FOLP/FOLP.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Martin D Coen, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8 -
     1.9 -Tactics and lemmas for FOLP (Classical First-Order Logic with Proofs)
    1.10 -*)
    1.11 -
    1.12 -(*** Classical introduction rules for | and EX ***)
    1.13 -
    1.14 -val prems= goal FOLP.thy 
    1.15 -   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
    1.16 -by (rtac classical 1);
    1.17 -by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
    1.18 -by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
    1.19 -qed "disjCI";
    1.20 -
    1.21 -(*introduction rule involving only EX*)
    1.22 -val prems= goal FOLP.thy 
    1.23 -   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    1.24 -by (rtac classical 1);
    1.25 -by (eresolve_tac (prems RL [exI]) 1) ;
    1.26 -qed "ex_classical";
    1.27 -
    1.28 -(*version of above, simplifying ~EX to ALL~ *)
    1.29 -val [prem]= goal FOLP.thy 
    1.30 -   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    1.31 -by (rtac ex_classical 1);
    1.32 -by (resolve_tac [notI RS allI RS prem] 1);
    1.33 -by (etac notE 1);
    1.34 -by (etac exI 1) ;
    1.35 -qed "exCI";
    1.36 -
    1.37 -val excluded_middle = prove_goal FOLP.thy "?p : ~P | P"
    1.38 - (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    1.39 -
    1.40 -
    1.41 -(*** Special elimination rules *)
    1.42 -
    1.43 -
    1.44 -(*Classical implies (-->) elimination. *)
    1.45 -val major::prems= goal FOLP.thy 
    1.46 -    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
    1.47 -by (resolve_tac [excluded_middle RS disjE] 1);
    1.48 -by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
    1.49 -qed "impCE";
    1.50 -
    1.51 -(*Double negation law*)
    1.52 -Goal "p:~~P ==> ?p : P";
    1.53 -by (rtac classical 1);
    1.54 -by (etac notE 1);
    1.55 -by (assume_tac 1);
    1.56 -qed "notnotD";
    1.57 -
    1.58 -
    1.59 -(*** Tactics for implication and contradiction ***)
    1.60 -
    1.61 -(*Classical <-> elimination.  Proof substitutes P=Q in 
    1.62 -    ~P ==> ~Q    and    P ==> Q  *)
    1.63 -val prems = goalw FOLP.thy [iff_def]
    1.64 -    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
    1.65 -\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
    1.66 -by (rtac conjE 1);
    1.67 -by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
    1.68 -               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
    1.69 -qed "iffCE";
    1.70 -
    1.71 -
    1.72 -(*Should be used as swap since ~P becomes redundant*)
    1.73 -val major::prems= goal FOLP.thy 
    1.74 -   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
    1.75 -by (rtac classical 1);
    1.76 -by (rtac (major RS notE) 1);
    1.77 -by (REPEAT (ares_tac prems 1)) ;
    1.78 -qed "swap";
    1.79 -
     2.1 --- a/src/FOLP/FOLP.thy	Sat Sep 17 20:49:14 2005 +0200
     2.2 +++ b/src/FOLP/FOLP.thy	Sun Sep 18 14:25:48 2005 +0200
     2.3 @@ -2,13 +2,88 @@
     2.4      ID:         $Id$
     2.5      Author:     Martin D Coen, Cambridge University Computer Laboratory
     2.6      Copyright   1992  University of Cambridge
     2.7 -
     2.8 -Classical First-Order Logic with Proofs
     2.9  *)
    2.10  
    2.11 -FOLP = IFOLP +
    2.12 +header {* Classical First-Order Logic with Proofs *}
    2.13 +
    2.14 +theory FOLP
    2.15 +imports IFOLP
    2.16 +uses
    2.17 +  ("FOLP_lemmas.ML") ("hypsubst.ML") ("classical.ML")
    2.18 +  ("simp.ML") ("intprover.ML") ("simpdata.ML")
    2.19 +begin
    2.20 +
    2.21  consts
    2.22    cla :: "[p=>p]=>p"
    2.23 -rules
    2.24 -  classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    2.25 +axioms
    2.26 +  classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    2.27 +
    2.28 +ML {* use_legacy_bindings (the_context ()) *}
    2.29 +
    2.30 +use "FOLP_lemmas.ML"
    2.31 +
    2.32 +use "hypsubst.ML"
    2.33 +use "classical.ML"      (* Patched 'cos matching won't instantiate proof *)
    2.34 +use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
    2.35 +
    2.36 +ML {*
    2.37 +
    2.38 +(*** Applying HypsubstFun to generate hyp_subst_tac ***)
    2.39 +
    2.40 +structure Hypsubst_Data =
    2.41 +  struct
    2.42 +  (*Take apart an equality judgement; otherwise raise Match!*)
    2.43 +  fun dest_eq (Const("Proof",_) $ (Const("op =",_)  $ t $ u) $ _) = (t,u);
    2.44 +
    2.45 +  val imp_intr = impI
    2.46 +
    2.47 +  (*etac rev_cut_eq moves an equality to be the last premise. *)
    2.48 +  val rev_cut_eq = prove_goal (the_context ())
    2.49 +                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
    2.50 +   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
    2.51 +
    2.52 +  val rev_mp = rev_mp
    2.53 +  val subst = subst
    2.54 +  val sym = sym
    2.55 +  val thin_refl = prove_goal (the_context ())
    2.56 +                  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
    2.57 +  end;
    2.58 +
    2.59 +structure Hypsubst = HypsubstFun(Hypsubst_Data);
    2.60 +open Hypsubst;
    2.61 +*}
    2.62 +
    2.63 +use "intprover.ML"
    2.64 +
    2.65 +ML {*
    2.66 +(*** Applying ClassicalFun to create a classical prover ***)
    2.67 +structure Classical_Data =
    2.68 +  struct
    2.69 +  val sizef = size_of_thm
    2.70 +  val mp = mp
    2.71 +  val not_elim = notE
    2.72 +  val swap = swap
    2.73 +  val hyp_subst_tacs=[hyp_subst_tac]
    2.74 +  end;
    2.75 +
    2.76 +structure Cla = ClassicalFun(Classical_Data);
    2.77 +open Cla;
    2.78 +
    2.79 +(*Propositional rules
    2.80 +  -- iffCE might seem better, but in the examples in ex/cla
    2.81 +     run about 7% slower than with iffE*)
    2.82 +val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    2.83 +                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    2.84 +
    2.85 +(*Quantifier rules*)
    2.86 +val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
    2.87 +                      addSEs [exE,ex1E] addEs [allE];
    2.88 +
    2.89 +val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
    2.90 +                          addSEs [exE,ex1E] addEs [all_dupE];
    2.91 +
    2.92 +*}
    2.93 +
    2.94 +use "simpdata.ML"
    2.95 +
    2.96  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/FOLP/FOLP_lemmas.ML	Sun Sep 18 14:25:48 2005 +0200
     3.3 @@ -0,0 +1,73 @@
     3.4 +(*  Title:      FOLP/FOLP.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Martin D Coen, Cambridge University Computer Laboratory
     3.7 +    Copyright   1991  University of Cambridge
     3.8 +*)
     3.9 +
    3.10 +(*** Classical introduction rules for | and EX ***)
    3.11 +
    3.12 +val prems= goal (the_context ())
    3.13 +   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
    3.14 +by (rtac classical 1);
    3.15 +by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
    3.16 +by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
    3.17 +qed "disjCI";
    3.18 +
    3.19 +(*introduction rule involving only EX*)
    3.20 +val prems= goal (the_context ())
    3.21 +   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    3.22 +by (rtac classical 1);
    3.23 +by (eresolve_tac (prems RL [exI]) 1) ;
    3.24 +qed "ex_classical";
    3.25 +
    3.26 +(*version of above, simplifying ~EX to ALL~ *)
    3.27 +val [prem]= goal (the_context ())
    3.28 +   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    3.29 +by (rtac ex_classical 1);
    3.30 +by (resolve_tac [notI RS allI RS prem] 1);
    3.31 +by (etac notE 1);
    3.32 +by (etac exI 1) ;
    3.33 +qed "exCI";
    3.34 +
    3.35 +val excluded_middle = prove_goal (the_context ()) "?p : ~P | P"
    3.36 + (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    3.37 +
    3.38 +
    3.39 +(*** Special elimination rules *)
    3.40 +
    3.41 +
    3.42 +(*Classical implies (-->) elimination. *)
    3.43 +val major::prems= goal (the_context ())
    3.44 +    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
    3.45 +by (resolve_tac [excluded_middle RS disjE] 1);
    3.46 +by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
    3.47 +qed "impCE";
    3.48 +
    3.49 +(*Double negation law*)
    3.50 +Goal "p:~~P ==> ?p : P";
    3.51 +by (rtac classical 1);
    3.52 +by (etac notE 1);
    3.53 +by (assume_tac 1);
    3.54 +qed "notnotD";
    3.55 +
    3.56 +
    3.57 +(*** Tactics for implication and contradiction ***)
    3.58 +
    3.59 +(*Classical <-> elimination.  Proof substitutes P=Q in
    3.60 +    ~P ==> ~Q    and    P ==> Q  *)
    3.61 +val prems = goalw (the_context ()) [iff_def]
    3.62 +    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
    3.63 +\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
    3.64 +by (rtac conjE 1);
    3.65 +by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
    3.66 +               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
    3.67 +qed "iffCE";
    3.68 +
    3.69 +
    3.70 +(*Should be used as swap since ~P becomes redundant*)
    3.71 +val major::prems= goal (the_context ())
    3.72 +   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
    3.73 +by (rtac classical 1);
    3.74 +by (rtac (major RS notE) 1);
    3.75 +by (REPEAT (ares_tac prems 1)) ;
    3.76 +qed "swap";
     4.1 --- a/src/FOLP/IFOLP.ML	Sat Sep 17 20:49:14 2005 +0200
     4.2 +++ b/src/FOLP/IFOLP.ML	Sun Sep 18 14:25:48 2005 +0200
     4.3 @@ -2,29 +2,28 @@
     4.4      ID:         $Id$
     4.5      Author:     Martin D Coen, Cambridge University Computer Laboratory
     4.6      Copyright   1992  University of Cambridge
     4.7 +*)
     4.8  
     4.9 -Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
    4.10 -*)
    4.11  (*** Sequent-style elimination rules for & --> and ALL ***)
    4.12  
    4.13 -val prems= Goal 
    4.14 +val prems= Goal
    4.15      "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R";
    4.16  by (REPEAT (resolve_tac prems 1
    4.17     ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ;
    4.18  qed "conjE";
    4.19  
    4.20 -val prems= Goal 
    4.21 +val prems= Goal
    4.22      "[| p:P-->Q;  q:P;  !!x. x:Q ==> r(x):R |] ==> ?p:R";
    4.23  by (REPEAT (resolve_tac (prems@[mp]) 1)) ;
    4.24  qed "impE";
    4.25  
    4.26 -val prems= Goal 
    4.27 +val prems= Goal
    4.28      "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R";
    4.29  by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
    4.30  qed "allE";
    4.31  
    4.32  (*Duplicates the quantifier; for use with eresolve_tac*)
    4.33 -val prems= Goal 
    4.34 +val prems= Goal
    4.35      "[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
    4.36  \    |] ==> ?p:R";
    4.37  by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
    4.38 @@ -33,16 +32,16 @@
    4.39  
    4.40  (*** Negation rules, which translate between ~P and P-->False ***)
    4.41  
    4.42 -val notI = prove_goalw IFOLP.thy [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
    4.43 +val notI = prove_goalw (the_context ()) [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
    4.44   (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
    4.45  
    4.46 -val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P;  q:P |] ==> ?p:R"
    4.47 +val notE = prove_goalw (the_context ()) [not_def] "[| p:~P;  q:P |] ==> ?p:R"
    4.48   (fn prems=>
    4.49    [ (resolve_tac [mp RS FalseE] 1),
    4.50      (REPEAT (resolve_tac prems 1)) ]);
    4.51  
    4.52  (*This is useful with the special implication rules for each kind of P. *)
    4.53 -val prems= Goal 
    4.54 +val prems= Goal
    4.55      "[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q";
    4.56  by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ;
    4.57  qed "not_to_imp";
    4.58 @@ -65,7 +64,7 @@
    4.59  
    4.60  (** Unique assumption tactic.
    4.61      Ignores proof objects.
    4.62 -    Fails unless one assumption is equal and exactly one is unifiable 
    4.63 +    Fails unless one assumption is equal and exactly one is unifiable
    4.64  **)
    4.65  
    4.66  local
    4.67 @@ -76,7 +75,7 @@
    4.68      (fn (prem,i) =>
    4.69        let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
    4.70            and concl = discard_proof (Logic.strip_assums_concl prem)
    4.71 -      in  
    4.72 +      in
    4.73            if exists (fn hyp => hyp aconv concl) hyps
    4.74            then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
    4.75                     [_] => assume_tac i
    4.76 @@ -97,22 +96,22 @@
    4.77  
    4.78  (*** If-and-only-if ***)
    4.79  
    4.80 -val iffI = prove_goalw IFOLP.thy [iff_def]
    4.81 +val iffI = prove_goalw (the_context ()) [iff_def]
    4.82     "[| !!x. x:P ==> q(x):Q;  !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
    4.83   (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
    4.84  
    4.85  
    4.86  (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
    4.87 -val iffE = prove_goalw IFOLP.thy [iff_def]
    4.88 +val iffE = prove_goalw (the_context ()) [iff_def]
    4.89      "[| p:P <-> Q;  !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R"
    4.90   (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);
    4.91  
    4.92  (* Destruct rules for <-> similar to Modus Ponens *)
    4.93  
    4.94 -val iffD1 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q;  q:P |] ==> ?p:Q"
    4.95 +val iffD1 = prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q;  q:P |] ==> ?p:Q"
    4.96   (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
    4.97  
    4.98 -val iffD2 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
    4.99 +val iffD2 = prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
   4.100   (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   4.101  
   4.102  Goal "?p:P <-> P";
   4.103 @@ -137,12 +136,12 @@
   4.104   do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   4.105  ***)
   4.106  
   4.107 -val prems = goalw IFOLP.thy [ex1_def]
   4.108 +val prems = goalw (the_context ()) [ex1_def]
   4.109      "[| p:P(a);  !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)";
   4.110  by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;
   4.111  qed "ex1I";
   4.112  
   4.113 -val prems = goalw IFOLP.thy [ex1_def]
   4.114 +val prems = goalw (the_context ()) [ex1_def]
   4.115      "[| p:EX! x. P(x);  \
   4.116  \       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
   4.117  \    ?a : R";
   4.118 @@ -158,7 +157,7 @@
   4.119      resolve_tac (prems RL [iffE]) i THEN
   4.120      REPEAT1 (eresolve_tac [asm_rl,mp] i);
   4.121  
   4.122 -val conj_cong = prove_goal IFOLP.thy 
   4.123 +val conj_cong = prove_goal (the_context ())
   4.124      "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
   4.125   (fn prems =>
   4.126    [ (cut_facts_tac prems 1),
   4.127 @@ -166,7 +165,7 @@
   4.128        ORELSE  eresolve_tac [iffE,conjE,mp] 1
   4.129        ORELSE  iff_tac prems 1)) ]);
   4.130  
   4.131 -val disj_cong = prove_goal IFOLP.thy 
   4.132 +val disj_cong = prove_goal (the_context ())
   4.133      "[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
   4.134   (fn prems =>
   4.135    [ (cut_facts_tac prems 1),
   4.136 @@ -174,7 +173,7 @@
   4.137        ORELSE  ares_tac [iffI] 1
   4.138        ORELSE  mp_tac 1)) ]);
   4.139  
   4.140 -val imp_cong = prove_goal IFOLP.thy 
   4.141 +val imp_cong = prove_goal (the_context ())
   4.142      "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
   4.143   (fn prems =>
   4.144    [ (cut_facts_tac prems 1),
   4.145 @@ -182,7 +181,7 @@
   4.146        ORELSE  etac iffE 1
   4.147        ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
   4.148  
   4.149 -val iff_cong = prove_goal IFOLP.thy 
   4.150 +val iff_cong = prove_goal (the_context ())
   4.151      "[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
   4.152   (fn prems =>
   4.153    [ (cut_facts_tac prems 1),
   4.154 @@ -190,7 +189,7 @@
   4.155        ORELSE  ares_tac [iffI] 1
   4.156        ORELSE  mp_tac 1)) ]);
   4.157  
   4.158 -val not_cong = prove_goal IFOLP.thy 
   4.159 +val not_cong = prove_goal (the_context ())
   4.160      "p:P <-> P' ==> ?p:~P <-> ~P'"
   4.161   (fn prems =>
   4.162    [ (cut_facts_tac prems 1),
   4.163 @@ -198,14 +197,14 @@
   4.164        ORELSE  mp_tac 1
   4.165        ORELSE  eresolve_tac [iffE,notE] 1)) ]);
   4.166  
   4.167 -val all_cong = prove_goal IFOLP.thy 
   4.168 +val all_cong = prove_goal (the_context ())
   4.169      "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
   4.170   (fn prems =>
   4.171    [ (REPEAT   (ares_tac [iffI,allI] 1
   4.172        ORELSE   mp_tac 1
   4.173        ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
   4.174  
   4.175 -val ex_cong = prove_goal IFOLP.thy 
   4.176 +val ex_cong = prove_goal (the_context ())
   4.177      "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
   4.178   (fn prems =>
   4.179    [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   4.180 @@ -213,7 +212,7 @@
   4.181        ORELSE   iff_tac prems 1)) ]);
   4.182  
   4.183  (*NOT PROVED
   4.184 -val ex1_cong = prove_goal IFOLP.thy 
   4.185 +val ex1_cong = prove_goal (the_context ())
   4.186      "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
   4.187   (fn prems =>
   4.188    [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
   4.189 @@ -225,8 +224,8 @@
   4.190  
   4.191  val refl = ieqI;
   4.192  
   4.193 -val subst = prove_goal IFOLP.thy "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
   4.194 - (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1), 
   4.195 +val subst = prove_goal (the_context ()) "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
   4.196 + (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1),
   4.197                          rtac impI 1, atac 1 ]);
   4.198  
   4.199  Goal "q:a=b ==> ?c:b=a";
   4.200 @@ -235,7 +234,7 @@
   4.201  qed "sym";
   4.202  
   4.203  Goal "[| p:a=b;  q:b=c |] ==> ?d:a=c";
   4.204 -by (etac subst 1 THEN assume_tac 1); 
   4.205 +by (etac subst 1 THEN assume_tac 1);
   4.206  qed "trans";
   4.207  
   4.208  (** ~ b=a ==> ~ a=b **)
   4.209 @@ -263,12 +262,12 @@
   4.210  qed "subst_context";
   4.211  
   4.212  Goal "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)";
   4.213 -by (REPEAT (etac ssubst 1)); 
   4.214 +by (REPEAT (etac ssubst 1));
   4.215  by (rtac refl 1) ;
   4.216  qed "subst_context2";
   4.217  
   4.218  Goal "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)";
   4.219 -by (REPEAT (etac ssubst 1)); 
   4.220 +by (REPEAT (etac ssubst 1));
   4.221  by (rtac refl 1) ;
   4.222  qed "subst_context3";
   4.223  
   4.224 @@ -309,8 +308,8 @@
   4.225  
   4.226  (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   4.227  
   4.228 -val pred_congs = 
   4.229 -    List.concat (map (fn c => 
   4.230 +val pred_congs =
   4.231 +    List.concat (map (fn c =>
   4.232                 map (fn th => read_instantiate [("P",c)] th)
   4.233                     [pred1_cong,pred2_cong,pred3_cong])
   4.234                 (explode"PQRS"));
   4.235 @@ -321,30 +320,30 @@
   4.236  
   4.237  (*** Simplifications of assumed implications.
   4.238       Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
   4.239 -     used with mp_tac (restricted to atomic formulae) is COMPLETE for 
   4.240 +     used with mp_tac (restricted to atomic formulae) is COMPLETE for
   4.241       intuitionistic propositional logic.  See
   4.242     R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   4.243      (preprint, University of St Andrews, 1991)  ***)
   4.244  
   4.245 -val major::prems= Goal 
   4.246 +val major::prems= Goal
   4.247      "[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R";
   4.248  by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ;
   4.249  qed "conj_impE";
   4.250  
   4.251 -val major::prems= Goal 
   4.252 +val major::prems= Goal
   4.253      "[| p:(P|Q)-->S;  !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R";
   4.254  by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ;
   4.255  qed "disj_impE";
   4.256  
   4.257 -(*Simplifies the implication.  Classical version is stronger. 
   4.258 +(*Simplifies the implication.  Classical version is stronger.
   4.259    Still UNSAFE since Q must be provable -- backtracking needed.  *)
   4.260 -val major::prems= Goal 
   4.261 +val major::prems= Goal
   4.262      "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
   4.263  \    ?p:R";
   4.264  by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ;
   4.265  qed "imp_impE";
   4.266  
   4.267 -(*Simplifies the implication.  Classical version is stronger. 
   4.268 +(*Simplifies the implication.  Classical version is stronger.
   4.269    Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   4.270  val major::prems= Goal
   4.271      "[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R";
   4.272 @@ -352,20 +351,20 @@
   4.273  qed "not_impE";
   4.274  
   4.275  (*Simplifies the implication.   UNSAFE.  *)
   4.276 -val major::prems= Goal 
   4.277 +val major::prems= Goal
   4.278      "[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
   4.279  \       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x. x:S ==> s(x):R |] ==> ?p:R";
   4.280  by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ;
   4.281  qed "iff_impE";
   4.282  
   4.283  (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   4.284 -val major::prems= Goal 
   4.285 +val major::prems= Goal
   4.286      "[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p:R";
   4.287  by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ;
   4.288  qed "all_impE";
   4.289  
   4.290  (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   4.291 -val major::prems= Goal 
   4.292 +val major::prems= Goal
   4.293      "[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R";
   4.294  by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ;
   4.295  qed "ex_impE";
     5.1 --- a/src/FOLP/IFOLP.thy	Sat Sep 17 20:49:14 2005 +0200
     5.2 +++ b/src/FOLP/IFOLP.thy	Sun Sep 18 14:25:48 2005 +0200
     5.3 @@ -2,30 +2,32 @@
     5.4      ID:         $Id$
     5.5      Author:     Martin D Coen, Cambridge University Computer Laboratory
     5.6      Copyright   1992  University of Cambridge
     5.7 -
     5.8 -Intuitionistic First-Order Logic with Proofs
     5.9  *)
    5.10  
    5.11 -IFOLP = Pure +
    5.12 +header {* Intuitionistic First-Order Logic with Proofs *}
    5.13 +
    5.14 +theory IFOLP
    5.15 +imports Pure
    5.16 +begin
    5.17  
    5.18  global
    5.19  
    5.20 -classes term
    5.21 -default term
    5.22 +classes "term"
    5.23 +defaultsort "term"
    5.24  
    5.25 -types
    5.26 -  p
    5.27 -  o
    5.28 +typedecl p
    5.29 +typedecl o
    5.30  
    5.31 -consts  
    5.32 +consts
    5.33        (*** Judgements ***)
    5.34   "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
    5.35   Proof          ::   "[o,p]=>prop"
    5.36   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    5.37 -        
    5.38 +
    5.39        (*** Logical Connectives -- Type Formers ***)
    5.40   "="            ::      "['a,'a] => o"  (infixl 50)
    5.41 - True,False     ::      "o"
    5.42 + True           ::      "o"
    5.43 + False          ::      "o"
    5.44   Not            ::      "o => o"        ("~ _" [40] 40)
    5.45   "&"            ::      "[o,o] => o"    (infixr 35)
    5.46   "|"            ::      "[o,o] => o"    (infixr 30)
    5.47 @@ -42,10 +44,12 @@
    5.48        (*** Proof Term Formers: precedence must exceed 50 ***)
    5.49   tt             :: "p"
    5.50   contr          :: "p=>p"
    5.51 - fst,snd        :: "p=>p"
    5.52 + fst            :: "p=>p"
    5.53 + snd            :: "p=>p"
    5.54   pair           :: "[p,p]=>p"           ("(1<_,/_>)")
    5.55   split          :: "[p, [p,p]=>p] =>p"
    5.56 - inl,inr        :: "p=>p"
    5.57 + inl            :: "p=>p"
    5.58 + inr            :: "p=>p"
    5.59   when           :: "[p, p=>p, p=>p]=>p"
    5.60   lambda         :: "(p => p) => p"      (binder "lam " 55)
    5.61   "`"            :: "[p,p]=>p"           (infixl 60)
    5.62 @@ -55,98 +59,103 @@
    5.63   xsplit         :: "[p,['a,p]=>p]=>p"
    5.64   ideq           :: "'a=>p"
    5.65   idpeel         :: "[p,'a=>p]=>p"
    5.66 - nrm, NRM       :: "p"
    5.67 + nrm            :: p
    5.68 + NRM            :: p
    5.69  
    5.70  local
    5.71  
    5.72 -rules
    5.73 +ML {*
    5.74 +
    5.75 +(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
    5.76 +val show_proofs = ref false;
    5.77 +
    5.78 +fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
    5.79 +
    5.80 +fun proof_tr' [P,p] =
    5.81 +    if !show_proofs then Const("@Proof",dummyT) $ p $ P
    5.82 +    else P  (*this case discards the proof term*);
    5.83 +*}
    5.84 +
    5.85 +parse_translation {* [("@Proof", proof_tr)] *}
    5.86 +print_translation {* [("Proof", proof_tr')] *}
    5.87 +
    5.88 +axioms
    5.89  
    5.90  (**** Propositional logic ****)
    5.91  
    5.92  (*Equality*)
    5.93  (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
    5.94  
    5.95 -ieqI      "ideq(a) : a=a"
    5.96 -ieqE      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    5.97 +ieqI:      "ideq(a) : a=a"
    5.98 +ieqE:      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    5.99  
   5.100  (* Truth and Falsity *)
   5.101  
   5.102 -TrueI     "tt : True"
   5.103 -FalseE    "a:False ==> contr(a):P"
   5.104 +TrueI:     "tt : True"
   5.105 +FalseE:    "a:False ==> contr(a):P"
   5.106  
   5.107  (* Conjunction *)
   5.108  
   5.109 -conjI     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
   5.110 -conjunct1 "p:P&Q ==> fst(p):P"
   5.111 -conjunct2 "p:P&Q ==> snd(p):Q"
   5.112 +conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
   5.113 +conjunct1: "p:P&Q ==> fst(p):P"
   5.114 +conjunct2: "p:P&Q ==> snd(p):Q"
   5.115  
   5.116  (* Disjunction *)
   5.117  
   5.118 -disjI1    "a:P ==> inl(a):P|Q"
   5.119 -disjI2    "b:Q ==> inr(b):P|Q"
   5.120 -disjE     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R 
   5.121 -          |] ==> when(a,f,g):R"
   5.122 +disjI1:    "a:P ==> inl(a):P|Q"
   5.123 +disjI2:    "b:Q ==> inr(b):P|Q"
   5.124 +disjE:     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R
   5.125 +           |] ==> when(a,f,g):R"
   5.126  
   5.127  (* Implication *)
   5.128  
   5.129 -impI      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
   5.130 -mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
   5.131 +impI:      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
   5.132 +mp:        "[| f:P-->Q;  a:P |] ==> f`a:Q"
   5.133  
   5.134  (*Quantifiers*)
   5.135  
   5.136 -allI      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
   5.137 -spec      "(f:ALL x. P(x)) ==> f^x : P(x)"
   5.138 +allI:      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
   5.139 +spec:      "(f:ALL x. P(x)) ==> f^x : P(x)"
   5.140  
   5.141 -exI       "p : P(x) ==> [x,p] : EX x. P(x)"
   5.142 -exE       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
   5.143 +exI:       "p : P(x) ==> [x,p] : EX x. P(x)"
   5.144 +exE:       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
   5.145  
   5.146  (**** Equality between proofs ****)
   5.147  
   5.148 -prefl     "a : P ==> a = a : P"
   5.149 -psym      "a = b : P ==> b = a : P"
   5.150 -ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
   5.151 +prefl:     "a : P ==> a = a : P"
   5.152 +psym:      "a = b : P ==> b = a : P"
   5.153 +ptrans:    "[| a = b : P;  b = c : P |] ==> a = c : P"
   5.154  
   5.155 -idpeelB   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
   5.156 +idpeelB:   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
   5.157  
   5.158 -fstB      "a:P ==> fst(<a,b>) = a : P"
   5.159 -sndB      "b:Q ==> snd(<a,b>) = b : Q"
   5.160 -pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
   5.161 +fstB:      "a:P ==> fst(<a,b>) = a : P"
   5.162 +sndB:      "b:Q ==> snd(<a,b>) = b : Q"
   5.163 +pairEC:    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
   5.164  
   5.165 -whenBinl  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
   5.166 -whenBinr  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
   5.167 -plusEC    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
   5.168 +whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
   5.169 +whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
   5.170 +plusEC:    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
   5.171  
   5.172 -applyB     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
   5.173 -funEC      "f:P ==> f = lam x. f`x : P"
   5.174 +applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
   5.175 +funEC:      "f:P ==> f = lam x. f`x : P"
   5.176  
   5.177 -specB      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
   5.178 +specB:      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
   5.179  
   5.180  
   5.181  (**** Definitions ****)
   5.182  
   5.183 -not_def              "~P == P-->False"
   5.184 -iff_def         "P<->Q == (P-->Q) & (Q-->P)"
   5.185 +not_def:              "~P == P-->False"
   5.186 +iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
   5.187  
   5.188  (*Unique existence*)
   5.189 -ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   5.190 +ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   5.191  
   5.192  (*Rewriting -- special constants to flag normalized terms and formulae*)
   5.193 -norm_eq "nrm : norm(x) = x"
   5.194 -NORM_iff        "NRM : NORM(P) <-> P"
   5.195 +norm_eq: "nrm : norm(x) = x"
   5.196 +NORM_iff:        "NRM : NORM(P) <-> P"
   5.197 +
   5.198 +ML {* use_legacy_bindings (the_context ()) *}
   5.199  
   5.200  end
   5.201  
   5.202 -ML
   5.203  
   5.204 -(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
   5.205 -val show_proofs = ref false;
   5.206 -
   5.207 -fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
   5.208 -
   5.209 -fun proof_tr' [P,p] = 
   5.210 -    if !show_proofs then Const("@Proof",dummyT) $ p $ P 
   5.211 -    else P  (*this case discards the proof term*);
   5.212 -
   5.213 -val  parse_translation = [("@Proof", proof_tr)];
   5.214 -val print_translation  = [("Proof", proof_tr')];
   5.215 -
     6.1 --- a/src/FOLP/IsaMakefile	Sat Sep 17 20:49:14 2005 +0200
     6.2 +++ b/src/FOLP/IsaMakefile	Sun Sep 18 14:25:48 2005 +0200
     6.3 @@ -26,7 +26,7 @@
     6.4  Pure:
     6.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     6.6  
     6.7 -$(OUT)/FOLP: $(OUT)/Pure FOLP.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
     6.8 +$(OUT)/FOLP: $(OUT)/Pure FOLP_lemmas.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
     6.9    classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
    6.10  	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
    6.11  
     7.1 --- a/src/FOLP/ROOT.ML	Sat Sep 17 20:49:14 2005 +0200
     7.2 +++ b/src/FOLP/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -(*  Title:      FOLP/ROOT
     7.5 +(*  Title:      FOLP/ROOT.ML
     7.6      ID:         $Id$
     7.7      Author:     martin Coen, Cambridge University Computer Laboratory
     7.8      Copyright   1993  University of Cambridge
     7.9 @@ -9,72 +9,6 @@
    7.10  *)
    7.11  
    7.12  val banner = "First-Order Logic with Natural Deduction with Proof Terms";
    7.13 -
    7.14  writeln banner;
    7.15  
    7.16 -print_depth 1;
    7.17 -
    7.18 -use_thy "IFOLP";
    7.19  use_thy "FOLP";
    7.20 -
    7.21 -use "hypsubst.ML";
    7.22 -use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
    7.23 -use "simp.ML";           (* Patched 'cos matching won't instantiate proof *)
    7.24 -
    7.25 -
    7.26 -(*** Applying HypsubstFun to generate hyp_subst_tac ***)
    7.27 -
    7.28 -structure Hypsubst_Data =
    7.29 -  struct
    7.30 -  (*Take apart an equality judgement; otherwise raise Match!*)
    7.31 -  fun dest_eq (Const("Proof",_) $ (Const("op =",_)  $ t $ u) $ _) = (t,u);
    7.32 -
    7.33 -  val imp_intr = impI
    7.34 -
    7.35 -  (*etac rev_cut_eq moves an equality to be the last premise. *)
    7.36 -  val rev_cut_eq = prove_goal IFOLP.thy 
    7.37 -                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
    7.38 -   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
    7.39 -
    7.40 -  val rev_mp = rev_mp
    7.41 -  val subst = subst
    7.42 -  val sym = sym
    7.43 -  val thin_refl = prove_goal IFOLP.thy 
    7.44 -		  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
    7.45 -  end;
    7.46 -
    7.47 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    7.48 -open Hypsubst;
    7.49 -
    7.50 -use "intprover.ML";
    7.51 -
    7.52 -(*** Applying ClassicalFun to create a classical prover ***)
    7.53 -structure Classical_Data = 
    7.54 -  struct
    7.55 -  val sizef = size_of_thm
    7.56 -  val mp = mp
    7.57 -  val not_elim = notE
    7.58 -  val swap = swap
    7.59 -  val hyp_subst_tacs=[hyp_subst_tac]
    7.60 -  end;
    7.61 -
    7.62 -structure Cla = ClassicalFun(Classical_Data);
    7.63 -open Cla;
    7.64 -
    7.65 -(*Propositional rules 
    7.66 -  -- iffCE might seem better, but in the examples in ex/cla
    7.67 -     run about 7% slower than with iffE*)
    7.68 -val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
    7.69 -                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    7.70 -
    7.71 -(*Quantifier rules*)
    7.72 -val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
    7.73 -                      addSEs [exE,ex1E] addEs [allE];
    7.74 -
    7.75 -val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] 
    7.76 -                          addSEs [exE,ex1E] addEs [all_dupE];
    7.77 -
    7.78 -use "simpdata.ML";
    7.79 -
    7.80 -
    7.81 -print_depth 8;
     8.1 --- a/src/FOLP/ex/If.ML	Sat Sep 17 20:49:14 2005 +0200
     8.2 +++ b/src/FOLP/ex/If.ML	Sun Sep 18 14:25:48 2005 +0200
     8.3 @@ -1,20 +1,15 @@
     8.4 -(*  Title:      FOLP/ex/if
     8.5 +(*  Title:      FOLP/ex/If.ML
     8.6      ID:         $Id$
     8.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.8      Copyright   1991  University of Cambridge
     8.9 -
    8.10 -For ex/if.thy.  First-Order Logic: the 'if' example
    8.11  *)
    8.12  
    8.13 -open If;
    8.14 -open Cla;    (*in case structure Int is open!*)
    8.15 -
    8.16 -val prems = goalw If.thy [if_def]
    8.17 +val prems = goalw (the_context ()) [if_def]
    8.18      "[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
    8.19  by (fast_tac (FOLP_cs addIs prems) 1);
    8.20  val ifI = result();
    8.21  
    8.22 -val major::prems = goalw If.thy [if_def]
    8.23 +val major::prems = goalw (the_context ()) [if_def]
    8.24     "[| p:if(P,Q,R);  !!x y.[| x:P; y:Q |] ==> f(x,y):S; \
    8.25  \                    !!x y.[| x:~P; y:R |] ==> g(x,y):S |] ==> ?p:S";
    8.26  by (cut_facts_tac [major] 1);
    8.27 @@ -39,5 +34,3 @@
    8.28  Goal "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
    8.29  by (fast_tac if_cs 1);
    8.30  val nested_ifs = result();
    8.31 -
    8.32 -writeln"Reached end of file.";
     9.1 --- a/src/FOLP/ex/If.thy	Sat Sep 17 20:49:14 2005 +0200
     9.2 +++ b/src/FOLP/ex/If.thy	Sun Sep 18 14:25:48 2005 +0200
     9.3 @@ -1,5 +1,13 @@
     9.4 -If = FOLP +
     9.5 -consts  if     :: "[o,o,o]=>o"
     9.6 -rules
     9.7 -        if_def "if(P,Q,R) == P&Q | ~P&R"
     9.8 +(* $Id$ *)
     9.9 +
    9.10 +theory If
    9.11 +imports FOLP
    9.12 +begin
    9.13 +
    9.14 +constdefs
    9.15 +  if :: "[o,o,o]=>o"
    9.16 +  "if(P,Q,R) == P&Q | ~P&R"
    9.17 +
    9.18 +ML {* use_legacy_bindings (the_context ()) *}
    9.19 +
    9.20  end
    10.1 --- a/src/FOLP/ex/Nat.ML	Sat Sep 17 20:49:14 2005 +0200
    10.2 +++ b/src/FOLP/ex/Nat.ML	Sun Sep 18 14:25:48 2005 +0200
    10.3 @@ -2,17 +2,8 @@
    10.4      ID:         $Id$
    10.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.6      Copyright   1992  University of Cambridge
    10.7 -
    10.8 -Examples for the manual "Introduction to Isabelle"
    10.9 -
   10.10 -Proofs about the natural numbers
   10.11 -
   10.12 -To generate similar output to manual, execute these commands:
   10.13 -    Pretty.setmargin 72; print_depth 0;
   10.14  *)
   10.15  
   10.16 -open Nat;
   10.17 -
   10.18  Goal "?p : ~ (Suc(k) = k)";
   10.19  by (res_inst_tac [("n","k")] induct 1);
   10.20  by (rtac notI 1);
   10.21 @@ -42,23 +33,23 @@
   10.22  val add_Suc = result();
   10.23  
   10.24  (*
   10.25 -val nat_congs = mk_congs Nat.thy ["Suc", "op +"];
   10.26 +val nat_congs = mk_congs (the_context ()) ["Suc", "op +"];
   10.27  prths nat_congs;
   10.28  *)
   10.29 -val prems = goal Nat.thy "p: x=y ==> ?p : Suc(x) = Suc(y)";
   10.30 +val prems = goal (the_context ()) "p: x=y ==> ?p : Suc(x) = Suc(y)";
   10.31  by (resolve_tac (prems RL [subst]) 1);
   10.32  by (rtac refl 1);
   10.33  val Suc_cong = result();
   10.34  
   10.35 -val prems = goal Nat.thy "[| p : a=x;  q: b=y |] ==> ?p : a+b=x+y";
   10.36 -by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN 
   10.37 +val prems = goal (the_context ()) "[| p : a=x;  q: b=y |] ==> ?p : a+b=x+y";
   10.38 +by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN
   10.39      rtac refl 1);
   10.40  val Plus_cong = result();
   10.41  
   10.42  val nat_congs = [Suc_cong,Plus_cong];
   10.43  
   10.44  
   10.45 -val add_ss = FOLP_ss  addcongs nat_congs  
   10.46 +val add_ss = FOLP_ss  addcongs nat_congs
   10.47                       addrews  [add_0, add_Suc];
   10.48  
   10.49  Goal "?p : (k+m)+n = k+(m+n)";
   10.50 @@ -79,4 +70,3 @@
   10.51  val add_Suc_right = result();
   10.52  
   10.53  (*mk_typed_congs appears not to work with FOLP's version of subst*)
   10.54 -
    11.1 --- a/src/FOLP/ex/Nat.thy	Sat Sep 17 20:49:14 2005 +0200
    11.2 +++ b/src/FOLP/ex/Nat.thy	Sun Sep 18 14:25:48 2005 +0200
    11.3 @@ -2,15 +2,16 @@
    11.4      ID:         $Id$
    11.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.6      Copyright   1992  University of Cambridge
    11.7 -
    11.8 -Examples for the manual "Introduction to Isabelle"
    11.9 -
   11.10 -Theory of the natural numbers: Peano's axioms, primitive recursion
   11.11  *)
   11.12  
   11.13 -Nat = IFOLP +
   11.14 -types   nat
   11.15 -arities nat         :: term
   11.16 +header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
   11.17 +
   11.18 +theory Nat
   11.19 +imports FOLP
   11.20 +begin
   11.21 +
   11.22 +typedecl nat
   11.23 +arities nat         :: "term"
   11.24  consts  "0"         :: "nat"    ("0")
   11.25          Suc         :: "nat=>nat"
   11.26          rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
   11.27 @@ -18,19 +19,24 @@
   11.28  
   11.29    (*Proof terms*)
   11.30         nrec         :: "[nat,p,[nat,p]=>p]=>p"
   11.31 -       ninj,nneq    :: "p=>p"
   11.32 -       rec0, recSuc :: "p"
   11.33 +       ninj         :: "p=>p"
   11.34 +       nneq         :: "p=>p"
   11.35 +       rec0         :: "p"
   11.36 +       recSuc       :: "p"
   11.37 +
   11.38 +axioms
   11.39 +  induct:     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
   11.40 +              |] ==> nrec(n,b,c):P(n)"
   11.41  
   11.42 -rules   
   11.43 -  induct     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x)) 
   11.44 -             |] ==> nrec(n,b,c):P(n)"
   11.45 -  
   11.46 -  Suc_inject "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
   11.47 -  Suc_neq_0  "p:Suc(m)=0      ==> nneq(p) : R"
   11.48 -  rec_0      "rec0 : rec(0,a,f) = a"
   11.49 -  rec_Suc    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
   11.50 -  add_def    "m+n == rec(m, n, %x y. Suc(y))"
   11.51 +  Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
   11.52 +  Suc_neq_0:  "p:Suc(m)=0      ==> nneq(p) : R"
   11.53 +  rec_0:      "rec0 : rec(0,a,f) = a"
   11.54 +  rec_Suc:    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
   11.55 +  add_def:    "m+n == rec(m, n, %x y. Suc(y))"
   11.56  
   11.57 -  nrecB0     "b: A ==> nrec(0,b,c) = b : A"
   11.58 -  nrecBSuc   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
   11.59 +  nrecB0:     "b: A ==> nrec(0,b,c) = b : A"
   11.60 +  nrecBSuc:   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
   11.61 +
   11.62 +ML {* use_legacy_bindings (the_context ()) *}
   11.63 +
   11.64  end
    12.1 --- a/src/FOLP/ex/ROOT.ML	Sat Sep 17 20:49:14 2005 +0200
    12.2 +++ b/src/FOLP/ex/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
    12.3 @@ -1,9 +1,9 @@
    12.4 -(*  Title:      FOLP/ex/ROOT
    12.5 +(*  Title:      FOLP/ex/ROOT.ML
    12.6      ID:         $Id$
    12.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.8      Copyright   1992  University of Cambridge
    12.9  
   12.10 -Executes all examples for First-Order Logic. 
   12.11 +Examples for First-Order Logic. 
   12.12  *)
   12.13  
   12.14  time_use     "intro.ML";
   12.15 @@ -13,7 +13,7 @@
   12.16  writeln"\n** Intuitionistic examples **\n";
   12.17  time_use     "int.ML";
   12.18  
   12.19 -val thy = IFOLP.thy  and  tac = IntPr.fast_tac 1;
   12.20 +val thy = theory "IFOLP"  and  tac = IntPr.fast_tac 1;
   12.21  time_use     "prop.ML";
   12.22  time_use     "quant.ML";
   12.23  
   12.24 @@ -21,6 +21,6 @@
   12.25  time_use     "cla.ML";
   12.26  time_use_thy "If";
   12.27  
   12.28 -val thy = FOLP.thy  and  tac = Cla.fast_tac FOLP_cs 1;
   12.29 +val thy = theory "FOLP"  and  tac = Cla.fast_tac FOLP_cs 1;
   12.30  time_use     "prop.ML";
   12.31  time_use     "quant.ML";
    13.1 --- a/src/FOLP/ex/cla.ML	Sat Sep 17 20:49:14 2005 +0200
    13.2 +++ b/src/FOLP/ex/cla.ML	Sun Sep 18 14:25:48 2005 +0200
    13.3 @@ -3,24 +3,20 @@
    13.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.5      Copyright   1993  University of Cambridge
    13.6  
    13.7 -Classical First-Order Logic
    13.8 +Classical First-Order Logic.
    13.9  *)
   13.10  
   13.11 -writeln"File FOLP/ex/cla.ML";
   13.12 -
   13.13 -open Cla;    (*in case structure Int is open!*)
   13.14 -
   13.15 -goal FOLP.thy "?p : (P --> Q | R) --> (P-->Q) | (P-->R)";
   13.16 +goal (theory "FOLP") "?p : (P --> Q | R) --> (P-->Q) | (P-->R)";
   13.17  by (fast_tac FOLP_cs 1);
   13.18  result();
   13.19  
   13.20  (*If and only if*)
   13.21  
   13.22 -goal FOLP.thy "?p : (P<->Q) <-> (Q<->P)";
   13.23 +goal (theory "FOLP") "?p : (P<->Q) <-> (Q<->P)";
   13.24  by (fast_tac FOLP_cs 1);
   13.25  result();
   13.26  
   13.27 -goal FOLP.thy "?p : ~ (P <-> ~P)";
   13.28 +goal (theory "FOLP") "?p : ~ (P <-> ~P)";
   13.29  by (fast_tac FOLP_cs 1);
   13.30  result();
   13.31  
   13.32 @@ -37,105 +33,105 @@
   13.33  
   13.34  writeln"Pelletier's examples";
   13.35  (*1*)
   13.36 -goal FOLP.thy "?p : (P-->Q)  <->  (~Q --> ~P)";
   13.37 +goal (theory "FOLP") "?p : (P-->Q)  <->  (~Q --> ~P)";
   13.38  by (fast_tac FOLP_cs 1);
   13.39  result();
   13.40  
   13.41  (*2*)
   13.42 -goal FOLP.thy "?p : ~ ~ P  <->  P";
   13.43 +goal (theory "FOLP") "?p : ~ ~ P  <->  P";
   13.44  by (fast_tac FOLP_cs 1);
   13.45  result();
   13.46  
   13.47  (*3*)
   13.48 -goal FOLP.thy "?p : ~(P-->Q) --> (Q-->P)";
   13.49 +goal (theory "FOLP") "?p : ~(P-->Q) --> (Q-->P)";
   13.50  by (fast_tac FOLP_cs 1);
   13.51  result();
   13.52  
   13.53  (*4*)
   13.54 -goal FOLP.thy "?p : (~P-->Q)  <->  (~Q --> P)";
   13.55 +goal (theory "FOLP") "?p : (~P-->Q)  <->  (~Q --> P)";
   13.56  by (fast_tac FOLP_cs 1);
   13.57  result();
   13.58  
   13.59  (*5*)
   13.60 -goal FOLP.thy "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))";
   13.61 +goal (theory "FOLP") "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))";
   13.62  by (fast_tac FOLP_cs 1);
   13.63  result();
   13.64  
   13.65  (*6*)
   13.66 -goal FOLP.thy "?p : P | ~ P";
   13.67 +goal (theory "FOLP") "?p : P | ~ P";
   13.68  by (fast_tac FOLP_cs 1);
   13.69  result();
   13.70  
   13.71  (*7*)
   13.72 -goal FOLP.thy "?p : P | ~ ~ ~ P";
   13.73 +goal (theory "FOLP") "?p : P | ~ ~ ~ P";
   13.74  by (fast_tac FOLP_cs 1);
   13.75  result();
   13.76  
   13.77  (*8.  Peirce's law*)
   13.78 -goal FOLP.thy "?p : ((P-->Q) --> P)  -->  P";
   13.79 +goal (theory "FOLP") "?p : ((P-->Q) --> P)  -->  P";
   13.80  by (fast_tac FOLP_cs 1);
   13.81  result();
   13.82  
   13.83  (*9*)
   13.84 -goal FOLP.thy "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   13.85 +goal (theory "FOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   13.86  by (fast_tac FOLP_cs 1);
   13.87  result();
   13.88  
   13.89  (*10*)
   13.90 -goal FOLP.thy "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";
   13.91 +goal (theory "FOLP") "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";
   13.92  by (fast_tac FOLP_cs 1);
   13.93  result();
   13.94  
   13.95  (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   13.96 -goal FOLP.thy "?p : P<->P";
   13.97 +goal (theory "FOLP") "?p : P<->P";
   13.98  by (fast_tac FOLP_cs 1);
   13.99  result();
  13.100  
  13.101  (*12.  "Dijkstra's law"*)
  13.102 -goal FOLP.thy "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
  13.103 +goal (theory "FOLP") "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
  13.104  by (fast_tac FOLP_cs 1);
  13.105  result();
  13.106  
  13.107  (*13.  Distributive law*)
  13.108 -goal FOLP.thy "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
  13.109 +goal (theory "FOLP") "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
  13.110  by (fast_tac FOLP_cs 1);
  13.111  result();
  13.112  
  13.113  (*14*)
  13.114 -goal FOLP.thy "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
  13.115 +goal (theory "FOLP") "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
  13.116  by (fast_tac FOLP_cs 1);
  13.117  result();
  13.118  
  13.119  (*15*)
  13.120 -goal FOLP.thy "?p : (P --> Q) <-> (~P | Q)";
  13.121 +goal (theory "FOLP") "?p : (P --> Q) <-> (~P | Q)";
  13.122  by (fast_tac FOLP_cs 1);
  13.123  result();
  13.124  
  13.125  (*16*)
  13.126 -goal FOLP.thy "?p : (P-->Q) | (Q-->P)";
  13.127 +goal (theory "FOLP") "?p : (P-->Q) | (Q-->P)";
  13.128  by (fast_tac FOLP_cs 1);
  13.129  result();
  13.130  
  13.131  (*17*)
  13.132 -goal FOLP.thy "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
  13.133 +goal (theory "FOLP") "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
  13.134  by (fast_tac FOLP_cs 1);
  13.135  result();
  13.136  
  13.137  writeln"Classical Logic: examples with quantifiers";
  13.138  
  13.139 -goal FOLP.thy "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
  13.140 +goal (theory "FOLP") "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
  13.141  by (fast_tac FOLP_cs 1);
  13.142  result(); 
  13.143  
  13.144 -goal FOLP.thy "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
  13.145 +goal (theory "FOLP") "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
  13.146  by (fast_tac FOLP_cs 1);
  13.147  result(); 
  13.148  
  13.149 -goal FOLP.thy "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
  13.150 +goal (theory "FOLP") "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
  13.151  by (fast_tac FOLP_cs 1);
  13.152  result(); 
  13.153  
  13.154 -goal FOLP.thy "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
  13.155 +goal (theory "FOLP") "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
  13.156  by (fast_tac FOLP_cs 1);
  13.157  result(); 
  13.158  
  13.159 @@ -143,16 +139,16 @@
  13.160  
  13.161  (*Needs multiple instantiation of ALL.*)
  13.162  (*
  13.163 -goal FOLP.thy "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
  13.164 +goal (theory "FOLP") "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
  13.165  by (best_tac FOLP_dup_cs 1);
  13.166  result();
  13.167  *)
  13.168  (*Needs double instantiation of the quantifier*)
  13.169 -goal FOLP.thy "?p : EX x. P(x) --> P(a) & P(b)";
  13.170 +goal (theory "FOLP") "?p : EX x. P(x) --> P(a) & P(b)";
  13.171  by (best_tac FOLP_dup_cs 1);
  13.172  result();
  13.173  
  13.174 -goal FOLP.thy "?p : EX z. P(z) --> (ALL x. P(x))";
  13.175 +goal (theory "FOLP") "?p : EX z. P(z) --> (ALL x. P(x))";
  13.176  by (best_tac FOLP_dup_cs 1);
  13.177  result();
  13.178  
  13.179 @@ -160,45 +156,45 @@
  13.180  writeln"Hard examples with quantifiers";
  13.181  
  13.182  writeln"Problem 18";
  13.183 -goal FOLP.thy "?p : EX y. ALL x. P(y)-->P(x)";
  13.184 +goal (theory "FOLP") "?p : EX y. ALL x. P(y)-->P(x)";
  13.185  by (best_tac FOLP_dup_cs 1);
  13.186  result(); 
  13.187  
  13.188  writeln"Problem 19";
  13.189 -goal FOLP.thy "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
  13.190 +goal (theory "FOLP") "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
  13.191  by (best_tac FOLP_dup_cs 1);
  13.192  result();
  13.193  
  13.194  writeln"Problem 20";
  13.195 -goal FOLP.thy "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
  13.196 +goal (theory "FOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
  13.197  \   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
  13.198  by (fast_tac FOLP_cs 1); 
  13.199  result();
  13.200  (*
  13.201  writeln"Problem 21";
  13.202 -goal FOLP.thy "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
  13.203 +goal (theory "FOLP") "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
  13.204  by (best_tac FOLP_dup_cs 1);
  13.205  result();
  13.206  *)
  13.207  writeln"Problem 22";
  13.208 -goal FOLP.thy "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
  13.209 +goal (theory "FOLP") "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
  13.210  by (fast_tac FOLP_cs 1); 
  13.211  result();
  13.212  
  13.213  writeln"Problem 23";
  13.214 -goal FOLP.thy "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
  13.215 +goal (theory "FOLP") "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
  13.216  by (best_tac FOLP_cs 1);  
  13.217  result();
  13.218  
  13.219  writeln"Problem 24";
  13.220 -goal FOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
  13.221 +goal (theory "FOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
  13.222  \    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
  13.223  \   --> (EX x. P(x)&R(x))";
  13.224  by (fast_tac FOLP_cs 1); 
  13.225  result();
  13.226  (*
  13.227  writeln"Problem 25";
  13.228 -goal FOLP.thy "?p : (EX x. P(x)) &  \
  13.229 +goal (theory "FOLP") "?p : (EX x. P(x)) &  \
  13.230  \       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
  13.231  \       (ALL x. P(x) --> (M(x) & L(x))) &   \
  13.232  \       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
  13.233 @@ -207,14 +203,14 @@
  13.234  result();
  13.235  
  13.236  writeln"Problem 26";
  13.237 -goal FOLP.thy "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   \
  13.238 +goal (theory "FOLP") "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   \
  13.239  \     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
  13.240  \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
  13.241  by (fast_tac FOLP_cs 1);
  13.242  result();
  13.243  *)
  13.244  writeln"Problem 27";
  13.245 -goal FOLP.thy "?p : (EX x. P(x) & ~Q(x)) &   \
  13.246 +goal (theory "FOLP") "?p : (EX x. P(x) & ~Q(x)) &   \
  13.247  \             (ALL x. P(x) --> R(x)) &   \
  13.248  \             (ALL x. M(x) & L(x) --> P(x)) &   \
  13.249  \             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
  13.250 @@ -223,7 +219,7 @@
  13.251  result();
  13.252  
  13.253  writeln"Problem 28.  AMENDED";
  13.254 -goal FOLP.thy "?p : (ALL x. P(x) --> (ALL x. Q(x))) &   \
  13.255 +goal (theory "FOLP") "?p : (ALL x. P(x) --> (ALL x. Q(x))) &   \
  13.256  \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
  13.257  \       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
  13.258  \   --> (ALL x. P(x) & L(x) --> M(x))";
  13.259 @@ -231,21 +227,21 @@
  13.260  result();
  13.261  
  13.262  writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
  13.263 -goal FOLP.thy "?p : (EX x. P(x)) & (EX y. Q(y))  \
  13.264 +goal (theory "FOLP") "?p : (EX x. P(x)) & (EX y. Q(y))  \
  13.265  \   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
  13.266  \        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
  13.267  by (fast_tac FOLP_cs 1); 
  13.268  result();
  13.269  
  13.270  writeln"Problem 30";
  13.271 -goal FOLP.thy "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & \
  13.272 +goal (theory "FOLP") "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & \
  13.273  \       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
  13.274  \   --> (ALL x. S(x))";
  13.275  by (fast_tac FOLP_cs 1);  
  13.276  result();
  13.277  
  13.278  writeln"Problem 31";
  13.279 -goal FOLP.thy "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
  13.280 +goal (theory "FOLP") "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
  13.281  \       (EX x. L(x) & P(x)) & \
  13.282  \       (ALL x. ~ R(x) --> M(x))  \
  13.283  \   --> (EX x. L(x) & M(x))";
  13.284 @@ -253,7 +249,7 @@
  13.285  result();
  13.286  
  13.287  writeln"Problem 32";
  13.288 -goal FOLP.thy "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
  13.289 +goal (theory "FOLP") "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
  13.290  \       (ALL x. S(x) & R(x) --> L(x)) & \
  13.291  \       (ALL x. M(x) --> R(x))  \
  13.292  \   --> (ALL x. P(x) & M(x) --> L(x))";
  13.293 @@ -261,18 +257,18 @@
  13.294  result();
  13.295  
  13.296  writeln"Problem 33";
  13.297 -goal FOLP.thy "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
  13.298 +goal (theory "FOLP") "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
  13.299  \    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
  13.300  by (best_tac FOLP_cs 1);
  13.301  result();
  13.302  
  13.303  writeln"Problem 35";
  13.304 -goal FOLP.thy "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))";
  13.305 +goal (theory "FOLP") "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))";
  13.306  by (best_tac FOLP_dup_cs 1);
  13.307  result();
  13.308  
  13.309  writeln"Problem 36";
  13.310 -goal FOLP.thy
  13.311 +goal (theory "FOLP")
  13.312  "?p : (ALL x. EX y. J(x,y)) & \
  13.313  \     (ALL x. EX y. G(x,y)) & \
  13.314  \     (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
  13.315 @@ -281,7 +277,7 @@
  13.316  result();
  13.317  
  13.318  writeln"Problem 37";
  13.319 -goal FOLP.thy "?p : (ALL z. EX w. ALL x. EX y. \
  13.320 +goal (theory "FOLP") "?p : (ALL z. EX w. ALL x. EX y. \
  13.321  \          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
  13.322  \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
  13.323  \       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
  13.324 @@ -290,24 +286,24 @@
  13.325  result();
  13.326  
  13.327  writeln"Problem 39";
  13.328 -goal FOLP.thy "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
  13.329 +goal (theory "FOLP") "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
  13.330  by (fast_tac FOLP_cs 1);
  13.331  result();
  13.332  
  13.333  writeln"Problem 40.  AMENDED";
  13.334 -goal FOLP.thy "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
  13.335 +goal (theory "FOLP") "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
  13.336  \             ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
  13.337  by (fast_tac FOLP_cs 1);
  13.338  result();
  13.339  
  13.340  writeln"Problem 41";
  13.341 -goal FOLP.thy "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))  \
  13.342 +goal (theory "FOLP") "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))  \
  13.343  \         --> ~ (EX z. ALL x. f(x,z))";
  13.344  by (best_tac FOLP_cs 1);
  13.345  result();
  13.346  
  13.347  writeln"Problem 44";
  13.348 -goal FOLP.thy "?p : (ALL x. f(x) -->                                    \
  13.349 +goal (theory "FOLP") "?p : (ALL x. f(x) -->                                    \
  13.350  \             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
  13.351  \             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
  13.352  \             --> (EX x. j(x) & ~f(x))";
  13.353 @@ -317,44 +313,42 @@
  13.354  writeln"Problems (mainly) involving equality or functions";
  13.355  
  13.356  writeln"Problem 48";
  13.357 -goal FOLP.thy "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
  13.358 +goal (theory "FOLP") "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
  13.359  by (fast_tac FOLP_cs 1);
  13.360  result();
  13.361  
  13.362  writeln"Problem 50";  
  13.363  (*What has this to do with equality?*)
  13.364 -goal FOLP.thy "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
  13.365 +goal (theory "FOLP") "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
  13.366  by (best_tac FOLP_dup_cs 1);
  13.367  result();
  13.368  
  13.369  writeln"Problem 56";
  13.370 -goal FOLP.thy
  13.371 +goal (theory "FOLP")
  13.372   "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
  13.373  by (fast_tac FOLP_cs 1);
  13.374  result();
  13.375  
  13.376  writeln"Problem 57";
  13.377 -goal FOLP.thy
  13.378 +goal (theory "FOLP")
  13.379  "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
  13.380  \     (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
  13.381  by (fast_tac FOLP_cs 1);
  13.382  result();
  13.383  
  13.384  writeln"Problem 58  NOT PROVED AUTOMATICALLY";
  13.385 -goal FOLP.thy "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
  13.386 +goal (theory "FOLP") "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
  13.387  val f_cong = read_instantiate [("t","f")] subst_context;
  13.388  by (fast_tac (FOLP_cs addIs [f_cong]) 1);
  13.389  result();
  13.390  
  13.391  writeln"Problem 59";
  13.392 -goal FOLP.thy "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
  13.393 +goal (theory "FOLP") "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
  13.394  by (best_tac FOLP_dup_cs 1);
  13.395  result();
  13.396  
  13.397  writeln"Problem 60";
  13.398 -goal FOLP.thy
  13.399 +goal (theory "FOLP")
  13.400  "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
  13.401  by (fast_tac FOLP_cs 1);
  13.402  result();
  13.403 -
  13.404 -writeln"Reached end of file.";
    14.1 --- a/src/FOLP/ex/foundn.ML	Sat Sep 17 20:49:14 2005 +0200
    14.2 +++ b/src/FOLP/ex/foundn.ML	Sun Sep 18 14:25:48 2005 +0200
    14.3 @@ -6,9 +6,7 @@
    14.4  Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
    14.5  *)
    14.6  
    14.7 -writeln"File FOLP/ex/foundn.ML";
    14.8 -
    14.9 -goal IFOLP.thy "?p : A&B  --> (C-->A&C)";
   14.10 +goal (theory "IFOLP") "?p : A&B  --> (C-->A&C)";
   14.11  by (rtac impI 1);
   14.12  by (rtac impI 1);
   14.13  by (rtac conjI 1);
   14.14 @@ -19,7 +17,7 @@
   14.15  
   14.16  (*A form of conj-elimination*)
   14.17  val prems = 
   14.18 -goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
   14.19 +goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
   14.20  by (resolve_tac prems 1);
   14.21  by (rtac conjunct1 1);
   14.22  by (resolve_tac prems 1);
   14.23 @@ -29,7 +27,7 @@
   14.24  
   14.25  
   14.26  val prems = 
   14.27 -goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
   14.28 +goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
   14.29  by (resolve_tac prems 1);
   14.30  by (rtac notI 1);
   14.31  by (res_inst_tac [ ("P", "~B") ]  notE  1);
   14.32 @@ -47,7 +45,7 @@
   14.33  
   14.34  
   14.35  val prems = 
   14.36 -goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
   14.37 +goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
   14.38  by (resolve_tac prems 1);
   14.39  by (rtac notI 1);
   14.40  by (rtac notE 1);
   14.41 @@ -61,7 +59,7 @@
   14.42  
   14.43  
   14.44  val prems = 
   14.45 -goal IFOLP.thy "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
   14.46 +goal (theory "IFOLP") "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
   14.47  by (rtac disjE 1);
   14.48  by (resolve_tac prems 1);
   14.49  by (assume_tac 1);
   14.50 @@ -75,7 +73,7 @@
   14.51  writeln"Examples with quantifiers";
   14.52  
   14.53  val prems =
   14.54 -goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
   14.55 +goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
   14.56  by (rtac allI 1);
   14.57  by (rtac disjI1 1);
   14.58  by (resolve_tac (prems RL [spec]) 1); 
   14.59 @@ -84,14 +82,14 @@
   14.60  result();
   14.61  
   14.62  
   14.63 -goal IFOLP.thy "?p : ALL x. EX y. x=y";
   14.64 +goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
   14.65  by (rtac allI 1);
   14.66  by (rtac exI 1);
   14.67  by (rtac refl 1);
   14.68  result();
   14.69  
   14.70  
   14.71 -goal IFOLP.thy "?p : EX y. ALL x. x=y";
   14.72 +goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
   14.73  by (rtac exI 1);
   14.74  by (rtac allI 1);
   14.75  by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
   14.76 @@ -99,7 +97,7 @@
   14.77  
   14.78  
   14.79  (*Parallel lifting example. *)
   14.80 -goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
   14.81 +goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
   14.82  by (resolve_tac [exI, allI] 1);
   14.83  by (resolve_tac [exI, allI] 1);
   14.84  by (resolve_tac [exI, allI] 1);
   14.85 @@ -108,7 +106,7 @@
   14.86  
   14.87  
   14.88  val prems =
   14.89 -goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
   14.90 +goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
   14.91  by (rtac conjE 1);
   14.92  by (resolve_tac prems 1);
   14.93  by (rtac exE 1);
   14.94 @@ -121,7 +119,7 @@
   14.95  
   14.96  
   14.97  (*A bigger demonstration of quantifiers -- not in the paper*)
   14.98 -goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
   14.99 +goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
  14.100  by (rtac impI 1);
  14.101  by (rtac allI 1);
  14.102  by (rtac exE 1 THEN assume_tac 1);
  14.103 @@ -129,6 +127,3 @@
  14.104  by (rtac allE 1 THEN assume_tac 1);
  14.105  by (assume_tac 1);
  14.106  result();  
  14.107 -
  14.108 -
  14.109 -writeln"Reached end of file.";
    15.1 --- a/src/FOLP/ex/int.ML	Sat Sep 17 20:49:14 2005 +0200
    15.2 +++ b/src/FOLP/ex/int.ML	Sun Sep 18 14:25:48 2005 +0200
    15.3 @@ -15,8 +15,6 @@
    15.4  by (IntPr.fast_tac 1);
    15.5  *)
    15.6  
    15.7 -writeln"File FOLP/ex/int.ML";
    15.8 -
    15.9  (*Note: for PROPOSITIONAL formulae...
   15.10    ~A is classically provable iff it is intuitionistically provable.  
   15.11    Therefore A is classically provable iff ~~A is intuitionistically provable.
   15.12 @@ -29,34 +27,34 @@
   15.13  ~~P is intuitionstically equivalent to P.  [Andy Pitts]
   15.14  *)
   15.15  
   15.16 -goal IFOLP.thy "?p : ~~(P&Q) <-> ~~P & ~~Q";
   15.17 +goal (theory "IFOLP") "?p : ~~(P&Q) <-> ~~P & ~~Q";
   15.18  by (IntPr.fast_tac 1);
   15.19  result();
   15.20  
   15.21 -goal IFOLP.thy "?p : ~~~P <-> ~P";
   15.22 +goal (theory "IFOLP") "?p : ~~~P <-> ~P";
   15.23  by (IntPr.fast_tac 1);
   15.24  result();
   15.25  
   15.26 -goal IFOLP.thy "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))";
   15.27 +goal (theory "IFOLP") "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))";
   15.28  by (IntPr.fast_tac 1);
   15.29  result();
   15.30  
   15.31 -goal IFOLP.thy "?p : (P<->Q) <-> (Q<->P)";
   15.32 +goal (theory "IFOLP") "?p : (P<->Q) <-> (Q<->P)";
   15.33  by (IntPr.fast_tac 1);
   15.34  result();
   15.35  
   15.36  
   15.37  writeln"Lemmas for the propositional double-negation translation";
   15.38  
   15.39 -goal IFOLP.thy "?p : P --> ~~P";
   15.40 +goal (theory "IFOLP") "?p : P --> ~~P";
   15.41  by (IntPr.fast_tac 1);
   15.42  result();
   15.43  
   15.44 -goal IFOLP.thy "?p : ~~(~~P --> P)";
   15.45 +goal (theory "IFOLP") "?p : ~~(~~P --> P)";
   15.46  by (IntPr.fast_tac 1);
   15.47  result();
   15.48  
   15.49 -goal IFOLP.thy "?p : ~~P & ~~(P --> Q) --> ~~Q";
   15.50 +goal (theory "IFOLP") "?p : ~~P & ~~(P --> Q) --> ~~Q";
   15.51  by (IntPr.fast_tac 1);
   15.52  result();
   15.53  
   15.54 @@ -64,12 +62,12 @@
   15.55  writeln"The following are classically but not constructively valid.";
   15.56  
   15.57  (*The attempt to prove them terminates quickly!*)
   15.58 -goal IFOLP.thy "?p : ((P-->Q) --> P)  -->  P";
   15.59 +goal (theory "IFOLP") "?p : ((P-->Q) --> P)  -->  P";
   15.60  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   15.61  (*Check that subgoals remain: proof failed.*)
   15.62  getgoal 1;  
   15.63  
   15.64 -goal IFOLP.thy "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)";
   15.65 +goal (theory "IFOLP") "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)";
   15.66  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   15.67  getgoal 1;  
   15.68  
   15.69 @@ -77,99 +75,99 @@
   15.70  writeln"Intuitionistic FOL: propositional problems based on Pelletier.";
   15.71  
   15.72  writeln"Problem ~~1";
   15.73 -goal IFOLP.thy "?p : ~~((P-->Q)  <->  (~Q --> ~P))";
   15.74 +goal (theory "IFOLP") "?p : ~~((P-->Q)  <->  (~Q --> ~P))";
   15.75  by (IntPr.fast_tac 1);
   15.76  result();
   15.77  (*5 secs*)
   15.78  
   15.79  
   15.80  writeln"Problem ~~2";
   15.81 -goal IFOLP.thy "?p : ~~(~~P  <->  P)";
   15.82 +goal (theory "IFOLP") "?p : ~~(~~P  <->  P)";
   15.83  by (IntPr.fast_tac 1);
   15.84  result();
   15.85  (*1 secs*)
   15.86  
   15.87  
   15.88  writeln"Problem 3";
   15.89 -goal IFOLP.thy "?p : ~(P-->Q) --> (Q-->P)";
   15.90 +goal (theory "IFOLP") "?p : ~(P-->Q) --> (Q-->P)";
   15.91  by (IntPr.fast_tac 1);
   15.92  result();
   15.93  
   15.94  writeln"Problem ~~4";
   15.95 -goal IFOLP.thy "?p : ~~((~P-->Q)  <->  (~Q --> P))";
   15.96 +goal (theory "IFOLP") "?p : ~~((~P-->Q)  <->  (~Q --> P))";
   15.97  by (IntPr.fast_tac 1);
   15.98  result();
   15.99  (*9 secs*)
  15.100  
  15.101  writeln"Problem ~~5";
  15.102 -goal IFOLP.thy "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
  15.103 +goal (theory "IFOLP") "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
  15.104  by (IntPr.fast_tac 1);
  15.105  result();
  15.106  (*10 secs*)
  15.107  
  15.108  
  15.109  writeln"Problem ~~6";
  15.110 -goal IFOLP.thy "?p : ~~(P | ~P)";
  15.111 +goal (theory "IFOLP") "?p : ~~(P | ~P)";
  15.112  by (IntPr.fast_tac 1);
  15.113  result();
  15.114  
  15.115  writeln"Problem ~~7";
  15.116 -goal IFOLP.thy "?p : ~~(P | ~~~P)";
  15.117 +goal (theory "IFOLP") "?p : ~~(P | ~~~P)";
  15.118  by (IntPr.fast_tac 1);
  15.119  result();
  15.120  
  15.121  writeln"Problem ~~8.  Peirce's law";
  15.122 -goal IFOLP.thy "?p : ~~(((P-->Q) --> P)  -->  P)";
  15.123 +goal (theory "IFOLP") "?p : ~~(((P-->Q) --> P)  -->  P)";
  15.124  by (IntPr.fast_tac 1);
  15.125  result();
  15.126  
  15.127  writeln"Problem 9";
  15.128 -goal IFOLP.thy "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  15.129 +goal (theory "IFOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  15.130  by (IntPr.fast_tac 1);
  15.131  result();
  15.132  (*9 secs*)
  15.133  
  15.134  
  15.135  writeln"Problem 10";
  15.136 -goal IFOLP.thy "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)";
  15.137 +goal (theory "IFOLP") "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)";
  15.138  by (IntPr.fast_tac 1);
  15.139  result();
  15.140  
  15.141  writeln"11.  Proved in each direction (incorrectly, says Pelletier!!) ";
  15.142 -goal IFOLP.thy "?p : P<->P";
  15.143 +goal (theory "IFOLP") "?p : P<->P";
  15.144  by (IntPr.fast_tac 1);
  15.145  
  15.146  writeln"Problem ~~12.  Dijkstra's law  ";
  15.147 -goal IFOLP.thy "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))";
  15.148 +goal (theory "IFOLP") "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))";
  15.149  by (IntPr.fast_tac 1);
  15.150  result();
  15.151  
  15.152 -goal IFOLP.thy "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))";
  15.153 +goal (theory "IFOLP") "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))";
  15.154  by (IntPr.fast_tac 1);
  15.155  result();
  15.156  
  15.157  writeln"Problem 13.  Distributive law";
  15.158 -goal IFOLP.thy "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
  15.159 +goal (theory "IFOLP") "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
  15.160  by (IntPr.fast_tac 1);
  15.161  result();
  15.162  
  15.163  writeln"Problem ~~14";
  15.164 -goal IFOLP.thy "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
  15.165 +goal (theory "IFOLP") "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
  15.166  by (IntPr.fast_tac 1);
  15.167  result();
  15.168  
  15.169  writeln"Problem ~~15";
  15.170 -goal IFOLP.thy "?p : ~~((P --> Q) <-> (~P | Q))";
  15.171 +goal (theory "IFOLP") "?p : ~~((P --> Q) <-> (~P | Q))";
  15.172  by (IntPr.fast_tac 1);
  15.173  result();
  15.174  
  15.175  writeln"Problem ~~16";
  15.176 -goal IFOLP.thy "?p : ~~((P-->Q) | (Q-->P))";
  15.177 +goal (theory "IFOLP") "?p : ~~((P-->Q) | (Q-->P))";
  15.178  by (IntPr.fast_tac 1);
  15.179  result();
  15.180  
  15.181  writeln"Problem ~~17";
  15.182 -goal IFOLP.thy
  15.183 +goal (theory "IFOLP")
  15.184    "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))";
  15.185  by (IntPr.fast_tac 1);
  15.186  (*over 5 minutes?? -- printing the proof term takes 40 secs!!*)
  15.187 @@ -180,23 +178,23 @@
  15.188  
  15.189  writeln"The converse is classical in the following implications...";
  15.190  
  15.191 -goal IFOLP.thy "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
  15.192 +goal (theory "IFOLP") "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
  15.193  by (IntPr.fast_tac 1); 
  15.194  result();  
  15.195  
  15.196 -goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
  15.197 +goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
  15.198  by (IntPr.fast_tac 1); 
  15.199  result();  
  15.200  
  15.201 -goal IFOLP.thy "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))";
  15.202 +goal (theory "IFOLP") "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))";
  15.203  by (IntPr.fast_tac 1); 
  15.204  result();  
  15.205  
  15.206 -goal IFOLP.thy "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
  15.207 +goal (theory "IFOLP") "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
  15.208  by (IntPr.fast_tac 1); 
  15.209  result();  
  15.210  
  15.211 -goal IFOLP.thy "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
  15.212 +goal (theory "IFOLP") "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
  15.213  by (IntPr.fast_tac 1);
  15.214  result();  
  15.215  
  15.216 @@ -206,24 +204,24 @@
  15.217  writeln"The following are not constructively valid!";
  15.218  (*The attempt to prove them terminates quickly!*)
  15.219  
  15.220 -goal IFOLP.thy "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
  15.221 +goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
  15.222  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
  15.223  getgoal 1; 
  15.224  
  15.225 -goal IFOLP.thy "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
  15.226 +goal (theory "IFOLP") "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
  15.227  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
  15.228  getgoal 1; 
  15.229  
  15.230 -goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
  15.231 +goal (theory "IFOLP") "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
  15.232  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
  15.233  getgoal 1; 
  15.234  
  15.235 -goal IFOLP.thy "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
  15.236 +goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
  15.237  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
  15.238  getgoal 1; 
  15.239  
  15.240  (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
  15.241 -goal IFOLP.thy "?p : EX x. Q(x) --> (ALL x. Q(x))";
  15.242 +goal (theory "IFOLP") "?p : EX x. Q(x) --> (ALL x. Q(x))";
  15.243  by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
  15.244  getgoal 1; 
  15.245  
  15.246 @@ -234,36 +232,36 @@
  15.247    Some will require quantifier duplication -- not currently available*)
  15.248  
  15.249  writeln"Problem ~~18";
  15.250 -goal IFOLP.thy "?p : ~~(EX y. ALL x. P(y)-->P(x))";
  15.251 +goal (theory "IFOLP") "?p : ~~(EX y. ALL x. P(y)-->P(x))";
  15.252  (*NOT PROVED*)
  15.253  
  15.254  writeln"Problem ~~19";
  15.255 -goal IFOLP.thy "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))";
  15.256 +goal (theory "IFOLP") "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))";
  15.257  (*NOT PROVED*)
  15.258  
  15.259  writeln"Problem 20";
  15.260 -goal IFOLP.thy "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
  15.261 +goal (theory "IFOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
  15.262  \   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
  15.263  by (IntPr.fast_tac 1); 
  15.264  result();
  15.265  
  15.266  writeln"Problem 21";
  15.267 -goal IFOLP.thy
  15.268 +goal (theory "IFOLP")
  15.269      "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))";
  15.270  (*NOT PROVED*)
  15.271  
  15.272  writeln"Problem 22";
  15.273 -goal IFOLP.thy "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
  15.274 +goal (theory "IFOLP") "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
  15.275  by (IntPr.fast_tac 1); 
  15.276  result();
  15.277  
  15.278  writeln"Problem ~~23";
  15.279 -goal IFOLP.thy "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))";
  15.280 +goal (theory "IFOLP") "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))";
  15.281  by (IntPr.best_tac 1);  
  15.282  result();
  15.283  
  15.284  writeln"Problem 24";
  15.285 -goal IFOLP.thy "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
  15.286 +goal (theory "IFOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
  15.287  \    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
  15.288  \   --> ~~(EX x. P(x)&R(x))";
  15.289  (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
  15.290 @@ -274,7 +272,7 @@
  15.291  result();
  15.292  
  15.293  writeln"Problem 25";
  15.294 -goal IFOLP.thy "?p : (EX x. P(x)) &  \
  15.295 +goal (theory "IFOLP") "?p : (EX x. P(x)) &  \
  15.296  \       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
  15.297  \       (ALL x. P(x) --> (M(x) & L(x))) &   \
  15.298  \       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
  15.299 @@ -283,21 +281,21 @@
  15.300  result();
  15.301  
  15.302  writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
  15.303 -goal IFOLP.thy "?p : (EX x. P(x)) & (EX y. Q(y))  \
  15.304 +goal (theory "IFOLP") "?p : (EX x. P(x)) & (EX y. Q(y))  \
  15.305  \   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
  15.306  \        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
  15.307  by (IntPr.fast_tac 1); 
  15.308  result();
  15.309  
  15.310  writeln"Problem ~~30";
  15.311 -goal IFOLP.thy "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & \
  15.312 +goal (theory "IFOLP") "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & \
  15.313  \       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
  15.314  \   --> (ALL x. ~~S(x))";
  15.315  by (IntPr.fast_tac 1);  
  15.316  result();
  15.317  
  15.318  writeln"Problem 31";
  15.319 -goal IFOLP.thy "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
  15.320 +goal (theory "IFOLP") "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
  15.321  \       (EX x. L(x) & P(x)) & \
  15.322  \       (ALL x. ~ R(x) --> M(x))  \
  15.323  \   --> (EX x. L(x) & M(x))";
  15.324 @@ -305,7 +303,7 @@
  15.325  result();
  15.326  
  15.327  writeln"Problem 32";
  15.328 -goal IFOLP.thy "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
  15.329 +goal (theory "IFOLP") "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
  15.330  \       (ALL x. S(x) & R(x) --> L(x)) & \
  15.331  \       (ALL x. M(x) --> R(x))  \
  15.332  \   --> (ALL x. P(x) & M(x) --> L(x))";
  15.333 @@ -313,18 +311,18 @@
  15.334  result();
  15.335  
  15.336  writeln"Problem 39";
  15.337 -goal IFOLP.thy "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
  15.338 +goal (theory "IFOLP") "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
  15.339  by (IntPr.fast_tac 1);
  15.340  result();
  15.341  
  15.342  writeln"Problem 40.  AMENDED";
  15.343 -goal IFOLP.thy "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
  15.344 +goal (theory "IFOLP") "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
  15.345  \             ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
  15.346  by (IntPr.fast_tac 1);
  15.347  result();
  15.348  
  15.349  writeln"Problem 44";
  15.350 -goal IFOLP.thy "?p : (ALL x. f(x) -->                                   \
  15.351 +goal (theory "IFOLP") "?p : (ALL x. f(x) -->                                   \
  15.352  \             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
  15.353  \             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
  15.354  \             --> (EX x. j(x) & ~f(x))";
  15.355 @@ -332,34 +330,32 @@
  15.356  result();
  15.357  
  15.358  writeln"Problem 48";
  15.359 -goal IFOLP.thy "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
  15.360 +goal (theory "IFOLP") "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
  15.361  by (IntPr.fast_tac 1);
  15.362  result();
  15.363  
  15.364  writeln"Problem 51";
  15.365 -goal IFOLP.thy
  15.366 +goal (theory "IFOLP")
  15.367      "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
  15.368  \    (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
  15.369  by (IntPr.best_tac 1);  (*60 seconds*)
  15.370  result();
  15.371  
  15.372  writeln"Problem 56";
  15.373 -goal IFOLP.thy
  15.374 +goal (theory "IFOLP")
  15.375      "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
  15.376  by (IntPr.fast_tac 1);
  15.377  result();
  15.378  
  15.379  writeln"Problem 57";
  15.380 -goal IFOLP.thy
  15.381 +goal (theory "IFOLP")
  15.382      "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
  15.383  \    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
  15.384  by (IntPr.fast_tac 1);
  15.385  result();
  15.386  
  15.387  writeln"Problem 60";
  15.388 -goal IFOLP.thy
  15.389 +goal (theory "IFOLP")
  15.390      "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
  15.391  by (IntPr.fast_tac 1);
  15.392  result();
  15.393 -
  15.394 -writeln"Reached end of file.";
    16.1 --- a/src/FOLP/ex/intro.ML	Sat Sep 17 20:49:14 2005 +0200
    16.2 +++ b/src/FOLP/ex/intro.ML	Sun Sep 18 14:25:48 2005 +0200
    16.3 @@ -14,7 +14,7 @@
    16.4  
    16.5  (**** Some simple backward proofs ****)
    16.6  
    16.7 -goal FOLP.thy "?p:P|P --> P";
    16.8 +goal (theory "FOLP") "?p:P|P --> P";
    16.9  by (rtac impI 1);
   16.10  by (rtac disjE 1);
   16.11  by (assume_tac 3);
   16.12 @@ -22,7 +22,7 @@
   16.13  by (assume_tac 1);
   16.14  val mythm = result();
   16.15  
   16.16 -goal FOLP.thy "?p:(P & Q) | R  --> (P | R)";
   16.17 +goal (theory "FOLP") "?p:(P & Q) | R  --> (P | R)";
   16.18  by (rtac impI 1);
   16.19  by (etac disjE 1);
   16.20  by (dtac conjunct1 1);
   16.21 @@ -32,7 +32,7 @@
   16.22  result();
   16.23  
   16.24  (*Correct version, delaying use of "spec" until last*)
   16.25 -goal FOLP.thy "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
   16.26 +goal (theory "FOLP") "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
   16.27  by (rtac impI 1);
   16.28  by (rtac allI 1);
   16.29  by (rtac allI 1);
   16.30 @@ -44,12 +44,12 @@
   16.31  
   16.32  (**** Demonstration of fast_tac ****)
   16.33  
   16.34 -goal FOLP.thy "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
   16.35 +goal (theory "FOLP") "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
   16.36  \       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
   16.37  by (fast_tac FOLP_cs 1);
   16.38  result();
   16.39  
   16.40 -goal FOLP.thy "?p:ALL x. P(x,f(x)) <-> \
   16.41 +goal (theory "FOLP") "?p:ALL x. P(x,f(x)) <-> \
   16.42  \       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
   16.43  by (fast_tac FOLP_cs 1);
   16.44  result();
   16.45 @@ -57,7 +57,7 @@
   16.46  
   16.47  (**** Derivation of conjunction elimination rule ****)
   16.48  
   16.49 -val [major,minor] = goal FOLP.thy "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
   16.50 +val [major,minor] = goal (theory "FOLP") "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
   16.51  by (rtac minor 1);
   16.52  by (resolve_tac [major RS conjunct1] 1);
   16.53  by (resolve_tac [major RS conjunct2] 1);
   16.54 @@ -69,14 +69,14 @@
   16.55  
   16.56  (** Derivation of negation introduction **)
   16.57  
   16.58 -val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P";
   16.59 +val prems = goal (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P";
   16.60  by (rewtac not_def);
   16.61  by (rtac impI 1);
   16.62  by (resolve_tac prems 1);
   16.63  by (assume_tac 1);
   16.64  result();
   16.65  
   16.66 -val [major,minor] = goal FOLP.thy "[| p:~P;  q:P |] ==> ?p:R";
   16.67 +val [major,minor] = goal (theory "FOLP") "[| p:~P;  q:P |] ==> ?p:R";
   16.68  by (rtac FalseE 1);
   16.69  by (rtac mp 1);
   16.70  by (resolve_tac [rewrite_rule [not_def] major] 1);
   16.71 @@ -84,9 +84,7 @@
   16.72  result();
   16.73  
   16.74  (*Alternative proof of above result*)
   16.75 -val [major,minor] = goalw FOLP.thy [not_def]
   16.76 +val [major,minor] = goalw (theory "FOLP") [not_def]
   16.77      "[| p:~P;  q:P |] ==> ?p:R";
   16.78  by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
   16.79  result();
   16.80 -
   16.81 -writeln"Reached end of file.";
    17.1 --- a/src/FOLP/ex/prop.ML	Sat Sep 17 20:49:14 2005 +0200
    17.2 +++ b/src/FOLP/ex/prop.ML	Sun Sep 18 14:25:48 2005 +0200
    17.3 @@ -7,9 +7,6 @@
    17.4  Needs declarations of the theory "thy" and the tactic "tac"
    17.5  *)
    17.6  
    17.7 -writeln"File FOLP/ex/prop.ML";
    17.8 -
    17.9 -
   17.10  writeln"commutative laws of & and | ";
   17.11  Goal "?p : P & Q  -->  Q & P";
   17.12  by tac;
   17.13 @@ -149,5 +146,3 @@
   17.14  \    --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5";
   17.15  by tac;
   17.16  result();
   17.17 -
   17.18 -writeln"Reached end of file.";
    18.1 --- a/src/FOLP/ex/quant.ML	Sat Sep 17 20:49:14 2005 +0200
    18.2 +++ b/src/FOLP/ex/quant.ML	Sun Sep 18 14:25:48 2005 +0200
    18.3 @@ -7,101 +7,99 @@
    18.4  Needs declarations of the theory "thy" and the tactic "tac"
    18.5  *)
    18.6  
    18.7 -writeln"File FOLP/ex/quant.ML";
    18.8 -
    18.9  Goal "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
   18.10  by tac;
   18.11 -result();  
   18.12 +result();
   18.13  
   18.14  
   18.15  Goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
   18.16  by tac;
   18.17 -result();  
   18.18 +result();
   18.19  
   18.20  
   18.21  (*Converse is false*)
   18.22  Goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
   18.23  by tac;
   18.24 -result();  
   18.25 +result();
   18.26  
   18.27  Goal "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
   18.28  by tac;
   18.29 -result();  
   18.30 +result();
   18.31  
   18.32  
   18.33  Goal "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
   18.34  by tac;
   18.35 -result();  
   18.36 +result();
   18.37  
   18.38  
   18.39  writeln"Some harder ones";
   18.40  
   18.41  Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
   18.42  by tac;
   18.43 -result();  
   18.44 +result();
   18.45  (*6 secs*)
   18.46  
   18.47  (*Converse is false*)
   18.48  Goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
   18.49  by tac;
   18.50 -result();  
   18.51 +result();
   18.52  
   18.53  
   18.54  writeln"Basic test of quantifier reasoning";
   18.55  (*TRUE*)
   18.56  Goal "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
   18.57 -by tac;  
   18.58 -result();  
   18.59 +by tac;
   18.60 +result();
   18.61  
   18.62  
   18.63  Goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))";
   18.64 -by tac;  
   18.65 -result();  
   18.66 +by tac;
   18.67 +result();
   18.68  
   18.69  
   18.70  writeln"The following should fail, as they are false!";
   18.71  
   18.72  Goal "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
   18.73 -by tac handle ERROR => writeln"Failed, as expected";  
   18.74 +by tac handle ERROR => writeln"Failed, as expected";
   18.75  (*Check that subgoals remain: proof failed.*)
   18.76 -getgoal 1; 
   18.77 +getgoal 1;
   18.78  
   18.79  Goal "?p : (EX x. Q(x))  -->  (ALL x. Q(x))";
   18.80 -by tac handle ERROR => writeln"Failed, as expected";  
   18.81 -getgoal 1; 
   18.82 +by tac handle ERROR => writeln"Failed, as expected";
   18.83 +getgoal 1;
   18.84  
   18.85  Goal "?p : P(?a) --> (ALL x. P(x))";
   18.86  by tac handle ERROR => writeln"Failed, as expected";
   18.87  (*Check that subgoals remain: proof failed.*)
   18.88 -getgoal 1;  
   18.89 +getgoal 1;
   18.90  
   18.91  Goal
   18.92      "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
   18.93  by tac handle ERROR => writeln"Failed, as expected";
   18.94 -getgoal 1;  
   18.95 +getgoal 1;
   18.96  
   18.97  
   18.98  writeln"Back to things that are provable...";
   18.99  
  18.100  Goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
  18.101 -by tac;  
  18.102 -result();  
  18.103 +by tac;
  18.104 +result();
  18.105  
  18.106  
  18.107  (*An example of why exI should be delayed as long as possible*)
  18.108  Goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
  18.109 -by tac;  
  18.110 -result();  
  18.111 +by tac;
  18.112 +result();
  18.113  
  18.114  Goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
  18.115 -by tac; 
  18.116 -(*Verify that no subgoals remain.*) 
  18.117 -uresult();  
  18.118 +by tac;
  18.119 +(*Verify that no subgoals remain.*)
  18.120 +uresult();
  18.121  
  18.122  
  18.123  Goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))";
  18.124  by tac;
  18.125 -result();  
  18.126 +result();
  18.127  
  18.128  
  18.129  writeln"Some slow ones";
  18.130 @@ -110,20 +108,17 @@
  18.131  (*Principia Mathematica *11.53  *)
  18.132  Goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
  18.133  by tac;
  18.134 -result();  
  18.135 +result();
  18.136  (*6 secs*)
  18.137  
  18.138  (*Principia Mathematica *11.55  *)
  18.139  Goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
  18.140  by tac;
  18.141 -result();  
  18.142 +result();
  18.143  (*9 secs*)
  18.144  
  18.145  (*Principia Mathematica *11.61  *)
  18.146  Goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
  18.147  by tac;
  18.148 -result();  
  18.149 +result();
  18.150  (*3 secs*)
  18.151 -
  18.152 -writeln"Reached end of file.";
  18.153 -
    19.1 --- a/src/FOLP/simpdata.ML	Sat Sep 17 20:49:14 2005 +0200
    19.2 +++ b/src/FOLP/simpdata.ML	Sun Sep 18 14:25:48 2005 +0200
    19.3 @@ -3,13 +3,13 @@
    19.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.5      Copyright   1991  University of Cambridge
    19.6  
    19.7 -Simplification data for FOLP
    19.8 +Simplification data for FOLP.
    19.9  *)
   19.10  
   19.11  (*** Rewrite rules ***)
   19.12  
   19.13 -fun int_prove_fun_raw s = 
   19.14 -    (writeln s;  prove_goal IFOLP.thy s
   19.15 +fun int_prove_fun_raw s =
   19.16 +    (writeln s;  prove_goal (the_context ()) s
   19.17         (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
   19.18  
   19.19  fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
   19.20 @@ -32,7 +32,7 @@
   19.21  
   19.22  val imp_rews = map int_prove_fun
   19.23   ["(P --> False) <-> ~P",       "(P --> True) <-> True",
   19.24 -  "(False --> P) <-> True",     "(True --> P) <-> P", 
   19.25 +  "(False --> P) <-> True",     "(True --> P) <-> P",
   19.26    "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
   19.27  
   19.28  val iff_rews = map int_prove_fun
   19.29 @@ -70,7 +70,7 @@
   19.30  fun mk_eq th = case concl_of th of
   19.31        _ $ (Const("op <->",_)$_$_) $ _ => th
   19.32      | _ $ (Const("op =",_)$_$_) $ _ => th
   19.33 -    | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F 
   19.34 +    | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
   19.35      | _ => make_iff_T th;
   19.36  
   19.37  
   19.38 @@ -113,12 +113,12 @@
   19.39  structure FOLP_Simp = SimpFun(FOLP_SimpData);
   19.40  
   19.41  (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
   19.42 -val FOLP_congs = 
   19.43 +val FOLP_congs =
   19.44     [all_cong,ex_cong,eq_cong,
   19.45      conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
   19.46  
   19.47  val IFOLP_rews =
   19.48 -   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ 
   19.49 +   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
   19.50      imp_rews @ iff_rews @ quant_rews;
   19.51  
   19.52  open FOLP_Simp;
   19.53 @@ -128,8 +128,8 @@
   19.54  val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
   19.55  
   19.56  (*Classical version...*)
   19.57 -fun prove_fun s = 
   19.58 -    (writeln s;  prove_goal FOLP.thy s
   19.59 +fun prove_fun s =
   19.60 +    (writeln s;  prove_goal (the_context ()) s
   19.61         (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
   19.62  
   19.63  val cla_rews = map prove_fun
   19.64 @@ -139,5 +139,3 @@
   19.65  val FOLP_rews = IFOLP_rews@cla_rews;
   19.66  
   19.67  val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;
   19.68 -
   19.69 -