converted legacy ML scripts;
authorwenzelm
Tue Mar 18 22:19:18 2008 +0100 (2008-03-18)
changeset 26322eaf634e975fa
parent 26321 d875e70a94de
child 26323 73efc70edeef
converted legacy ML scripts;
src/FOLP/FOLP.thy
src/FOLP/FOLP_lemmas.ML
src/FOLP/IFOLP.ML
src/FOLP/IFOLP.thy
src/FOLP/IsaMakefile
src/FOLP/ex/Classical.thy
src/FOLP/ex/Intuitionistic.thy
src/FOLP/ex/ROOT.ML
src/FOLP/ex/cla.ML
src/FOLP/ex/int.ML
src/FOLP/intprover.ML
src/FOLP/simpdata.ML
     1.1 --- a/src/FOLP/FOLP.thy	Tue Mar 18 21:57:36 2008 +0100
     1.2 +++ b/src/FOLP/FOLP.thy	Tue Mar 18 22:19:18 2008 +0100
     1.3 @@ -9,8 +9,7 @@
     1.4  theory FOLP
     1.5  imports IFOLP
     1.6  uses
     1.7 -  ("FOLP_lemmas.ML") ("hypsubst.ML") ("classical.ML")
     1.8 -  ("simp.ML") ("intprover.ML") ("simpdata.ML")
     1.9 +  ("classical.ML") ("simp.ML") ("simpdata.ML")
    1.10  begin
    1.11  
    1.12  consts
    1.13 @@ -18,52 +17,104 @@
    1.14  axioms
    1.15    classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    1.16  
    1.17 -ML {* use_legacy_bindings (the_context ()) *}
    1.18 +
    1.19 +(*** Classical introduction rules for | and EX ***)
    1.20 +
    1.21 +lemma disjCI:
    1.22 +  assumes "!!x. x:~Q ==> f(x):P"
    1.23 +  shows "?p : P|Q"
    1.24 +  apply (rule classical)
    1.25 +  apply (assumption | rule assms disjI1 notI)+
    1.26 +  apply (assumption | rule disjI2 notE)+
    1.27 +  done
    1.28 +
    1.29 +(*introduction rule involving only EX*)
    1.30 +lemma ex_classical:
    1.31 +  assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"
    1.32 +  shows "?p : EX x. P(x)"
    1.33 +  apply (rule classical)
    1.34 +  apply (rule exI, rule assms, assumption)
    1.35 +  done
    1.36 +
    1.37 +(*version of above, simplifying ~EX to ALL~ *)
    1.38 +lemma exCI:
    1.39 +  assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"
    1.40 +  shows "?p : EX x. P(x)"
    1.41 +  apply (rule ex_classical)
    1.42 +  apply (rule notI [THEN allI, THEN assms])
    1.43 +  apply (erule notE)
    1.44 +  apply (erule exI)
    1.45 +  done
    1.46 +
    1.47 +lemma excluded_middle: "?p : ~P | P"
    1.48 +  apply (rule disjCI)
    1.49 +  apply assumption
    1.50 +  done
    1.51 +
    1.52 +
    1.53 +(*** Special elimination rules *)
    1.54  
    1.55 -use "FOLP_lemmas.ML"
    1.56 +(*Classical implies (-->) elimination. *)
    1.57 +lemma impCE:
    1.58 +  assumes major: "p:P-->Q"
    1.59 +    and r1: "!!x. x:~P ==> f(x):R"
    1.60 +    and r2: "!!y. y:Q ==> g(y):R"
    1.61 +  shows "?p : R"
    1.62 +  apply (rule excluded_middle [THEN disjE])
    1.63 +   apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
    1.64 +       resolve_tac [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *})
    1.65 +  done
    1.66 +
    1.67 +(*Double negation law*)
    1.68 +lemma notnotD: "p:~~P ==> ?p : P"
    1.69 +  apply (rule classical)
    1.70 +  apply (erule notE)
    1.71 +  apply assumption
    1.72 +  done
    1.73 +
    1.74 +
    1.75 +(*** Tactics for implication and contradiction ***)
    1.76  
    1.77 -use "hypsubst.ML"
    1.78 +(*Classical <-> elimination.  Proof substitutes P=Q in
    1.79 +    ~P ==> ~Q    and    P ==> Q  *)
    1.80 +lemma iffCE:
    1.81 +  assumes major: "p:P<->Q"
    1.82 +    and r1: "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
    1.83 +    and r2: "!!x y.[| x:~P; y:~Q |] ==> g(x,y):R"
    1.84 +  shows "?p : R"
    1.85 +  apply (insert major)
    1.86 +  apply (unfold iff_def)
    1.87 +  apply (rule conjE)
    1.88 +  apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE
    1.89 +      eresolve_tac [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE
    1.90 +      resolve_tac [@{thm r1}, @{thm r2}] 1) *})+
    1.91 +  done
    1.92 +
    1.93 +
    1.94 +(*Should be used as swap since ~P becomes redundant*)
    1.95 +lemma swap:
    1.96 +  assumes major: "p:~P"
    1.97 +    and r: "!!x. x:~Q ==> f(x):P"
    1.98 +  shows "?p : Q"
    1.99 +  apply (rule classical)
   1.100 +  apply (rule major [THEN notE])
   1.101 +  apply (rule r)
   1.102 +  apply assumption
   1.103 +  done
   1.104 +
   1.105  use "classical.ML"      (* Patched 'cos matching won't instantiate proof *)
   1.106  use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)
   1.107  
   1.108  ML {*
   1.109 -
   1.110 -(*** Applying HypsubstFun to generate hyp_subst_tac ***)
   1.111 -
   1.112 -structure Hypsubst_Data =
   1.113 -  struct
   1.114 -  (*Take apart an equality judgement; otherwise raise Match!*)
   1.115 -  fun dest_eq (Const("Proof",_) $ (Const("op =",_)  $ t $ u) $ _) = (t,u);
   1.116 -
   1.117 -  val imp_intr = impI
   1.118 -
   1.119 -  (*etac rev_cut_eq moves an equality to be the last premise. *)
   1.120 -  val rev_cut_eq = prove_goal @{theory}
   1.121 -                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
   1.122 -   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
   1.123 -
   1.124 -  val rev_mp = rev_mp
   1.125 -  val subst = subst
   1.126 -  val sym = sym
   1.127 -  val thin_refl = prove_goal @{theory} "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
   1.128 -  end;
   1.129 -
   1.130 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
   1.131 -open Hypsubst;
   1.132 -*}
   1.133 -
   1.134 -use "intprover.ML"
   1.135 -
   1.136 -ML {*
   1.137  (*** Applying ClassicalFun to create a classical prover ***)
   1.138  structure Classical_Data =
   1.139 -  struct
   1.140 +struct
   1.141    val sizef = size_of_thm
   1.142 -  val mp = mp
   1.143 -  val not_elim = notE
   1.144 -  val swap = swap
   1.145 -  val hyp_subst_tacs=[hyp_subst_tac]
   1.146 -  end;
   1.147 +  val mp = @{thm mp}
   1.148 +  val not_elim = @{thm notE}
   1.149 +  val swap = @{thm swap}
   1.150 +  val hyp_subst_tacs = [hyp_subst_tac]
   1.151 +end;
   1.152  
   1.153  structure Cla = ClassicalFun(Classical_Data);
   1.154  open Cla;
   1.155 @@ -71,17 +122,28 @@
   1.156  (*Propositional rules
   1.157    -- iffCE might seem better, but in the examples in ex/cla
   1.158       run about 7% slower than with iffE*)
   1.159 -val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
   1.160 -                       addSEs [conjE,disjE,impCE,FalseE,iffE];
   1.161 +val prop_cs =
   1.162 +  empty_cs addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI},
   1.163 +      @{thm impI}, @{thm notI}, @{thm iffI}]
   1.164 +    addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffE}];
   1.165  
   1.166  (*Quantifier rules*)
   1.167 -val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
   1.168 -                      addSEs [exE,ex1E] addEs [allE];
   1.169 +val FOLP_cs =
   1.170 +  prop_cs addSIs [@{thm allI}] addIs [@{thm exI}, @{thm ex1I}]
   1.171 +    addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm allE}];
   1.172  
   1.173 -val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
   1.174 -                          addSEs [exE,ex1E] addEs [all_dupE];
   1.175 +val FOLP_dup_cs =
   1.176 +  prop_cs addSIs [@{thm allI}] addIs [@{thm exCI}, @{thm ex1I}]
   1.177 +    addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];
   1.178 +*}
   1.179  
   1.180 -*}
   1.181 +lemma cla_rews:
   1.182 +  "?p1 : P | ~P"
   1.183 +  "?p2 : ~P | P"
   1.184 +  "?p3 : ~ ~ P <-> P"
   1.185 +  "?p4 : (~P --> P) <-> P"
   1.186 +  apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})
   1.187 +  done
   1.188  
   1.189  use "simpdata.ML"
   1.190  
     2.1 --- a/src/FOLP/FOLP_lemmas.ML	Tue Mar 18 21:57:36 2008 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,73 +0,0 @@
     2.4 -(*  Title:      FOLP/FOLP_lemmas.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Martin D Coen, Cambridge University Computer Laboratory
     2.7 -    Copyright   1991  University of Cambridge
     2.8 -*)
     2.9 -
    2.10 -(*** Classical introduction rules for | and EX ***)
    2.11 -
    2.12 -val prems= goal (the_context ())
    2.13 -   "(!!x. x:~Q ==> f(x):P) ==> ?p : P|Q";
    2.14 -by (rtac classical 1);
    2.15 -by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
    2.16 -by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
    2.17 -qed "disjCI";
    2.18 -
    2.19 -(*introduction rule involving only EX*)
    2.20 -val prems= goal (the_context ())
    2.21 -   "( !!u. u:~(EX x. P(x)) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    2.22 -by (rtac classical 1);
    2.23 -by (eresolve_tac (prems RL [exI]) 1) ;
    2.24 -qed "ex_classical";
    2.25 -
    2.26 -(*version of above, simplifying ~EX to ALL~ *)
    2.27 -val [prem]= goal (the_context ())
    2.28 -   "(!!u. u:ALL x. ~P(x) ==> f(u):P(a)) ==> ?p : EX x. P(x)";
    2.29 -by (rtac ex_classical 1);
    2.30 -by (resolve_tac [notI RS allI RS prem] 1);
    2.31 -by (etac notE 1);
    2.32 -by (etac exI 1) ;
    2.33 -qed "exCI";
    2.34 -
    2.35 -val excluded_middle = prove_goal (the_context ()) "?p : ~P | P"
    2.36 - (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    2.37 -
    2.38 -
    2.39 -(*** Special elimination rules *)
    2.40 -
    2.41 -
    2.42 -(*Classical implies (-->) elimination. *)
    2.43 -val major::prems= goal (the_context ())
    2.44 -    "[| p:P-->Q;  !!x. x:~P ==> f(x):R;  !!y. y:Q ==> g(y):R |] ==> ?p : R";
    2.45 -by (resolve_tac [excluded_middle RS disjE] 1);
    2.46 -by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
    2.47 -qed "impCE";
    2.48 -
    2.49 -(*Double negation law*)
    2.50 -Goal "p:~~P ==> ?p : P";
    2.51 -by (rtac classical 1);
    2.52 -by (etac notE 1);
    2.53 -by (assume_tac 1);
    2.54 -qed "notnotD";
    2.55 -
    2.56 -
    2.57 -(*** Tactics for implication and contradiction ***)
    2.58 -
    2.59 -(*Classical <-> elimination.  Proof substitutes P=Q in
    2.60 -    ~P ==> ~Q    and    P ==> Q  *)
    2.61 -val prems = goalw (the_context ()) [iff_def]
    2.62 -    "[| p:P<->Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R;  \
    2.63 -\                !!x y.[| x:~P; y:~Q |] ==> g(x,y):R |] ==> ?p : R";
    2.64 -by (rtac conjE 1);
    2.65 -by (REPEAT (DEPTH_SOLVE_1 (etac impCE 1
    2.66 -               ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ;
    2.67 -qed "iffCE";
    2.68 -
    2.69 -
    2.70 -(*Should be used as swap since ~P becomes redundant*)
    2.71 -val major::prems= goal (the_context ())
    2.72 -   "p:~P ==> (!!x. x:~Q ==> f(x):P) ==> ?p : Q";
    2.73 -by (rtac classical 1);
    2.74 -by (rtac (major RS notE) 1);
    2.75 -by (REPEAT (ares_tac prems 1)) ;
    2.76 -qed "swap";
     3.1 --- a/src/FOLP/IFOLP.ML	Tue Mar 18 21:57:36 2008 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,370 +0,0 @@
     3.4 -(*  Title:      FOLP/IFOLP.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Martin D Coen, Cambridge University Computer Laboratory
     3.7 -    Copyright   1992  University of Cambridge
     3.8 -*)
     3.9 -
    3.10 -(*** Sequent-style elimination rules for & --> and ALL ***)
    3.11 -
    3.12 -val prems= Goal
    3.13 -    "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R";
    3.14 -by (REPEAT (resolve_tac prems 1
    3.15 -   ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ;
    3.16 -qed "conjE";
    3.17 -
    3.18 -val prems= Goal
    3.19 -    "[| p:P-->Q;  q:P;  !!x. x:Q ==> r(x):R |] ==> ?p:R";
    3.20 -by (REPEAT (resolve_tac (prems@[mp]) 1)) ;
    3.21 -qed "impE";
    3.22 -
    3.23 -val prems= Goal
    3.24 -    "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R";
    3.25 -by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
    3.26 -qed "allE";
    3.27 -
    3.28 -(*Duplicates the quantifier; for use with eresolve_tac*)
    3.29 -val prems= Goal
    3.30 -    "[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
    3.31 -\    |] ==> ?p:R";
    3.32 -by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
    3.33 -qed "all_dupE";
    3.34 -
    3.35 -
    3.36 -(*** Negation rules, which translate between ~P and P-->False ***)
    3.37 -
    3.38 -bind_thm ("notI", prove_goalw (the_context ()) [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
    3.39 - (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]));
    3.40 -
    3.41 -bind_thm ("notE", prove_goalw (the_context ()) [not_def] "[| p:~P;  q:P |] ==> ?p:R"
    3.42 - (fn prems=>
    3.43 -  [ (resolve_tac [mp RS FalseE] 1),
    3.44 -    (REPEAT (resolve_tac prems 1)) ]));
    3.45 -
    3.46 -(*This is useful with the special implication rules for each kind of P. *)
    3.47 -val prems= Goal
    3.48 -    "[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q";
    3.49 -by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ;
    3.50 -qed "not_to_imp";
    3.51 -
    3.52 -
    3.53 -(* For substitution int an assumption P, reduce Q to P-->Q, substitute into
    3.54 -   this implication, then apply impI to move P back into the assumptions.
    3.55 -   To specify P use something like
    3.56 -      eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
    3.57 -Goal "[| p:P;  q:P --> Q |] ==> ?p:Q";
    3.58 -by (REPEAT (ares_tac [mp] 1)) ;
    3.59 -qed "rev_mp";
    3.60 -
    3.61 -
    3.62 -(*Contrapositive of an inference rule*)
    3.63 -val [major,minor]= Goal "[| p:~Q;  !!y. y:P==>q(y):Q |] ==> ?a:~P";
    3.64 -by (rtac (major RS notE RS notI) 1);
    3.65 -by (etac minor 1) ;
    3.66 -qed "contrapos";
    3.67 -
    3.68 -(** Unique assumption tactic.
    3.69 -    Ignores proof objects.
    3.70 -    Fails unless one assumption is equal and exactly one is unifiable
    3.71 -**)
    3.72 -
    3.73 -local
    3.74 -    fun discard_proof (Const("Proof",_) $ P $ _) = P;
    3.75 -in
    3.76 -val uniq_assume_tac =
    3.77 -  SUBGOAL
    3.78 -    (fn (prem,i) =>
    3.79 -      let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
    3.80 -          and concl = discard_proof (Logic.strip_assums_concl prem)
    3.81 -      in
    3.82 -          if exists (fn hyp => hyp aconv concl) hyps
    3.83 -          then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
    3.84 -                   [_] => assume_tac i
    3.85 -                 |  _  => no_tac
    3.86 -          else no_tac
    3.87 -      end);
    3.88 -end;
    3.89 -
    3.90 -
    3.91 -(*** Modus Ponens Tactics ***)
    3.92 -
    3.93 -(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    3.94 -fun mp_tac i = eresolve_tac [notE,make_elim mp] i  THEN  assume_tac i;
    3.95 -
    3.96 -(*Like mp_tac but instantiates no variables*)
    3.97 -fun int_uniq_mp_tac i = eresolve_tac [notE,impE] i  THEN  uniq_assume_tac i;
    3.98 -
    3.99 -
   3.100 -(*** If-and-only-if ***)
   3.101 -
   3.102 -bind_thm ("iffI", prove_goalw (the_context ()) [iff_def]
   3.103 -   "[| !!x. x:P ==> q(x):Q;  !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
   3.104 - (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]));
   3.105 -
   3.106 -
   3.107 -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   3.108 -bind_thm ("iffE", prove_goalw (the_context ()) [iff_def]
   3.109 -    "[| p:P <-> Q;  !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R"
   3.110 - (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]));
   3.111 -
   3.112 -(* Destruct rules for <-> similar to Modus Ponens *)
   3.113 -
   3.114 -bind_thm ("iffD1", prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q;  q:P |] ==> ?p:Q"
   3.115 - (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]));
   3.116 -
   3.117 -bind_thm ("iffD2", prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
   3.118 - (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]));
   3.119 -
   3.120 -Goal "?p:P <-> P";
   3.121 -by (REPEAT (ares_tac [iffI] 1)) ;
   3.122 -qed "iff_refl";
   3.123 -
   3.124 -Goal "p:Q <-> P ==> ?p:P <-> Q";
   3.125 -by (etac iffE 1);
   3.126 -by (rtac iffI 1);
   3.127 -by (REPEAT (eresolve_tac [asm_rl,mp] 1)) ;
   3.128 -qed "iff_sym";
   3.129 -
   3.130 -Goal "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R";
   3.131 -by (rtac iffI 1);
   3.132 -by (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ;
   3.133 -qed "iff_trans";
   3.134 -
   3.135 -
   3.136 -(*** Unique existence.  NOTE THAT the following 2 quantifications
   3.137 -   EX!x such that [EX!y such that P(x,y)]     (sequential)
   3.138 -   EX!x,y such that P(x,y)                    (simultaneous)
   3.139 - do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   3.140 -***)
   3.141 -
   3.142 -val prems = goalw (the_context ()) [ex1_def]
   3.143 -    "[| p:P(a);  !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)";
   3.144 -by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;
   3.145 -qed "ex1I";
   3.146 -
   3.147 -val prems = goalw (the_context ()) [ex1_def]
   3.148 -    "[| p:EX! x. P(x);  \
   3.149 -\       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
   3.150 -\    ?a : R";
   3.151 -by (cut_facts_tac prems 1);
   3.152 -by (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ;
   3.153 -qed "ex1E";
   3.154 -
   3.155 -
   3.156 -(*** <-> congruence rules for simplification ***)
   3.157 -
   3.158 -(*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
   3.159 -fun iff_tac prems i =
   3.160 -    resolve_tac (prems RL [iffE]) i THEN
   3.161 -    REPEAT1 (eresolve_tac [asm_rl,mp] i);
   3.162 -
   3.163 -bind_thm ("conj_cong", prove_goal (the_context ())
   3.164 -    "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
   3.165 - (fn prems =>
   3.166 -  [ (cut_facts_tac prems 1),
   3.167 -    (REPEAT  (ares_tac [iffI,conjI] 1
   3.168 -      ORELSE  eresolve_tac [iffE,conjE,mp] 1
   3.169 -      ORELSE  iff_tac prems 1)) ]));
   3.170 -
   3.171 -bind_thm ("disj_cong", prove_goal (the_context ())
   3.172 -    "[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
   3.173 - (fn prems =>
   3.174 -  [ (cut_facts_tac prems 1),
   3.175 -    (REPEAT  (eresolve_tac [iffE,disjE,disjI1,disjI2] 1
   3.176 -      ORELSE  ares_tac [iffI] 1
   3.177 -      ORELSE  mp_tac 1)) ]));
   3.178 -
   3.179 -bind_thm ("imp_cong", prove_goal (the_context ())
   3.180 -    "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
   3.181 - (fn prems =>
   3.182 -  [ (cut_facts_tac prems 1),
   3.183 -    (REPEAT   (ares_tac [iffI,impI] 1
   3.184 -      ORELSE  etac iffE 1
   3.185 -      ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]));
   3.186 -
   3.187 -bind_thm ("iff_cong", prove_goal (the_context ())
   3.188 -    "[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
   3.189 - (fn prems =>
   3.190 -  [ (cut_facts_tac prems 1),
   3.191 -    (REPEAT   (etac iffE 1
   3.192 -      ORELSE  ares_tac [iffI] 1
   3.193 -      ORELSE  mp_tac 1)) ]));
   3.194 -
   3.195 -bind_thm ("not_cong", prove_goal (the_context ())
   3.196 -    "p:P <-> P' ==> ?p:~P <-> ~P'"
   3.197 - (fn prems =>
   3.198 -  [ (cut_facts_tac prems 1),
   3.199 -    (REPEAT   (ares_tac [iffI,notI] 1
   3.200 -      ORELSE  mp_tac 1
   3.201 -      ORELSE  eresolve_tac [iffE,notE] 1)) ]));
   3.202 -
   3.203 -bind_thm ("all_cong", prove_goal (the_context ())
   3.204 -    "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
   3.205 - (fn prems =>
   3.206 -  [ (REPEAT   (ares_tac [iffI,allI] 1
   3.207 -      ORELSE   mp_tac 1
   3.208 -      ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]));
   3.209 -
   3.210 -bind_thm ("ex_cong", prove_goal (the_context ())
   3.211 -    "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
   3.212 - (fn prems =>
   3.213 -  [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   3.214 -      ORELSE   mp_tac 1
   3.215 -      ORELSE   iff_tac prems 1)) ]));
   3.216 -
   3.217 -(*NOT PROVED
   3.218 -bind_thm ("ex1_cong", prove_goal (the_context ())
   3.219 -    "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
   3.220 - (fn prems =>
   3.221 -  [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
   3.222 -      ORELSE   mp_tac 1
   3.223 -      ORELSE   iff_tac prems 1)) ]));
   3.224 -*)
   3.225 -
   3.226 -(*** Equality rules ***)
   3.227 -
   3.228 -bind_thm ("refl", ieqI);
   3.229 -
   3.230 -bind_thm ("subst", prove_goal (the_context ()) "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
   3.231 - (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1),
   3.232 -                        rtac impI 1, atac 1 ]));
   3.233 -
   3.234 -Goal "q:a=b ==> ?c:b=a";
   3.235 -by (etac subst 1);
   3.236 -by (rtac refl 1) ;
   3.237 -qed "sym";
   3.238 -
   3.239 -Goal "[| p:a=b;  q:b=c |] ==> ?d:a=c";
   3.240 -by (etac subst 1 THEN assume_tac 1);
   3.241 -qed "trans";
   3.242 -
   3.243 -(** ~ b=a ==> ~ a=b **)
   3.244 -Goal "p:~ b=a ==> ?q:~ a=b";
   3.245 -by (etac contrapos 1);
   3.246 -by (etac sym 1) ;
   3.247 -qed "not_sym";
   3.248 -
   3.249 -(*calling "standard" reduces maxidx to 0*)
   3.250 -bind_thm ("ssubst", standard (sym RS subst));
   3.251 -
   3.252 -(*A special case of ex1E that would otherwise need quantifier expansion*)
   3.253 -Goal "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b";
   3.254 -by (etac ex1E 1);
   3.255 -by (rtac trans 1);
   3.256 -by (rtac sym 2);
   3.257 -by (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ;
   3.258 -qed "ex1_equalsE";
   3.259 -
   3.260 -(** Polymorphic congruence rules **)
   3.261 -
   3.262 -Goal "[| p:a=b |]  ==>  ?d:t(a)=t(b)";
   3.263 -by (etac ssubst 1);
   3.264 -by (rtac refl 1) ;
   3.265 -qed "subst_context";
   3.266 -
   3.267 -Goal "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)";
   3.268 -by (REPEAT (etac ssubst 1));
   3.269 -by (rtac refl 1) ;
   3.270 -qed "subst_context2";
   3.271 -
   3.272 -Goal "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)";
   3.273 -by (REPEAT (etac ssubst 1));
   3.274 -by (rtac refl 1) ;
   3.275 -qed "subst_context3";
   3.276 -
   3.277 -(*Useful with eresolve_tac for proving equalties from known equalities.
   3.278 -        a = b
   3.279 -        |   |
   3.280 -        c = d   *)
   3.281 -Goal "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d";
   3.282 -by (rtac trans 1);
   3.283 -by (rtac trans 1);
   3.284 -by (rtac sym 1);
   3.285 -by (REPEAT (assume_tac 1)) ;
   3.286 -qed "box_equals";
   3.287 -
   3.288 -(*Dual of box_equals: for proving equalities backwards*)
   3.289 -Goal "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b";
   3.290 -by (rtac trans 1);
   3.291 -by (rtac trans 1);
   3.292 -by (REPEAT (eresolve_tac [asm_rl, sym] 1)) ;
   3.293 -qed "simp_equals";
   3.294 -
   3.295 -(** Congruence rules for predicate letters **)
   3.296 -
   3.297 -Goal "p:a=a' ==> ?p:P(a) <-> P(a')";
   3.298 -by (rtac iffI 1);
   3.299 -by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
   3.300 -qed "pred1_cong";
   3.301 -
   3.302 -Goal "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')";
   3.303 -by (rtac iffI 1);
   3.304 -by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
   3.305 -qed "pred2_cong";
   3.306 -
   3.307 -Goal "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')";
   3.308 -by (rtac iffI 1);
   3.309 -by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
   3.310 -qed "pred3_cong";
   3.311 -
   3.312 -(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   3.313 -
   3.314 -bind_thms ("pred_congs",
   3.315 -    List.concat (map (fn c =>
   3.316 -               map (fn th => read_instantiate [("P",c)] th)
   3.317 -                   [pred1_cong,pred2_cong,pred3_cong])
   3.318 -               (explode"PQRS")));
   3.319 -
   3.320 -(*special case for the equality predicate!*)
   3.321 -bind_thm ("eq_cong", read_instantiate [("P","op =")] pred2_cong);
   3.322 -
   3.323 -
   3.324 -(*** Simplifications of assumed implications.
   3.325 -     Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
   3.326 -     used with mp_tac (restricted to atomic formulae) is COMPLETE for
   3.327 -     intuitionistic propositional logic.  See
   3.328 -   R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   3.329 -    (preprint, University of St Andrews, 1991)  ***)
   3.330 -
   3.331 -val major::prems= Goal
   3.332 -    "[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R";
   3.333 -by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ;
   3.334 -qed "conj_impE";
   3.335 -
   3.336 -val major::prems= Goal
   3.337 -    "[| p:(P|Q)-->S;  !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R";
   3.338 -by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ;
   3.339 -qed "disj_impE";
   3.340 -
   3.341 -(*Simplifies the implication.  Classical version is stronger.
   3.342 -  Still UNSAFE since Q must be provable -- backtracking needed.  *)
   3.343 -val major::prems= Goal
   3.344 -    "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
   3.345 -\    ?p:R";
   3.346 -by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ;
   3.347 -qed "imp_impE";
   3.348 -
   3.349 -(*Simplifies the implication.  Classical version is stronger.
   3.350 -  Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   3.351 -val major::prems= Goal
   3.352 -    "[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R";
   3.353 -by (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ;
   3.354 -qed "not_impE";
   3.355 -
   3.356 -(*Simplifies the implication.   UNSAFE.  *)
   3.357 -val major::prems= Goal
   3.358 -    "[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
   3.359 -\       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x. x:S ==> s(x):R |] ==> ?p:R";
   3.360 -by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ;
   3.361 -qed "iff_impE";
   3.362 -
   3.363 -(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   3.364 -val major::prems= Goal
   3.365 -    "[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p:R";
   3.366 -by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ;
   3.367 -qed "all_impE";
   3.368 -
   3.369 -(*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   3.370 -val major::prems= Goal
   3.371 -    "[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R";
   3.372 -by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ;
   3.373 -qed "ex_impE";
     4.1 --- a/src/FOLP/IFOLP.thy	Tue Mar 18 21:57:36 2008 +0100
     4.2 +++ b/src/FOLP/IFOLP.thy	Tue Mar 18 22:19:18 2008 +0100
     4.3 @@ -8,6 +8,7 @@
     4.4  
     4.5  theory IFOLP
     4.6  imports Pure
     4.7 +uses ("hypsubst.ML") ("intprover.ML")
     4.8  begin
     4.9  
    4.10  global
    4.11 @@ -69,7 +70,7 @@
    4.12  (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
    4.13  val show_proofs = ref false;
    4.14  
    4.15 -fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
    4.16 +fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
    4.17  
    4.18  fun proof_tr' [P,p] =
    4.19      if !show_proofs then Const("@Proof",dummyT) $ p $ P
    4.20 @@ -154,8 +155,555 @@
    4.21  norm_eq: "nrm : norm(x) = x"
    4.22  NORM_iff:        "NRM : NORM(P) <-> P"
    4.23  
    4.24 -ML {* use_legacy_bindings (the_context ()) *}
    4.25 +(*** Sequent-style elimination rules for & --> and ALL ***)
    4.26 +
    4.27 +lemma conjE:
    4.28 +  assumes "p:P&Q"
    4.29 +    and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
    4.30 +  shows "?a:R"
    4.31 +  apply (rule assms(2))
    4.32 +   apply (rule conjunct1 [OF assms(1)])
    4.33 +  apply (rule conjunct2 [OF assms(1)])
    4.34 +  done
    4.35 +
    4.36 +lemma impE:
    4.37 +  assumes "p:P-->Q"
    4.38 +    and "q:P"
    4.39 +    and "!!x. x:Q ==> r(x):R"
    4.40 +  shows "?p:R"
    4.41 +  apply (rule assms mp)+
    4.42 +  done
    4.43 +
    4.44 +lemma allE:
    4.45 +  assumes "p:ALL x. P(x)"
    4.46 +    and "!!y. y:P(x) ==> q(y):R"
    4.47 +  shows "?p:R"
    4.48 +  apply (rule assms spec)+
    4.49 +  done
    4.50 +
    4.51 +(*Duplicates the quantifier; for use with eresolve_tac*)
    4.52 +lemma all_dupE:
    4.53 +  assumes "p:ALL x. P(x)"
    4.54 +    and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
    4.55 +  shows "?p:R"
    4.56 +  apply (rule assms spec)+
    4.57 +  done
    4.58 +
    4.59 +
    4.60 +(*** Negation rules, which translate between ~P and P-->False ***)
    4.61 +
    4.62 +lemma notI:
    4.63 +  assumes "!!x. x:P ==> q(x):False"
    4.64 +  shows "?p:~P"
    4.65 +  unfolding not_def
    4.66 +  apply (assumption | rule assms impI)+
    4.67 +  done
    4.68 +
    4.69 +lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
    4.70 +  unfolding not_def
    4.71 +  apply (drule (1) mp)
    4.72 +  apply (erule FalseE)
    4.73 +  done
    4.74 +
    4.75 +(*This is useful with the special implication rules for each kind of P. *)
    4.76 +lemma not_to_imp:
    4.77 +  assumes "p:~P"
    4.78 +    and "!!x. x:(P-->False) ==> q(x):Q"
    4.79 +  shows "?p:Q"
    4.80 +  apply (assumption | rule assms impI notE)+
    4.81 +  done
    4.82 +
    4.83 +(* For substitution int an assumption P, reduce Q to P-->Q, substitute into
    4.84 +   this implication, then apply impI to move P back into the assumptions.
    4.85 +   To specify P use something like
    4.86 +      eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
    4.87 +lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
    4.88 +  apply (assumption | rule mp)+
    4.89 +  done
    4.90 +
    4.91 +
    4.92 +(*Contrapositive of an inference rule*)
    4.93 +lemma contrapos:
    4.94 +  assumes major: "p:~Q"
    4.95 +    and minor: "!!y. y:P==>q(y):Q"
    4.96 +  shows "?a:~P"
    4.97 +  apply (rule major [THEN notE, THEN notI])
    4.98 +  apply (erule minor)
    4.99 +  done
   4.100 +
   4.101 +(** Unique assumption tactic.
   4.102 +    Ignores proof objects.
   4.103 +    Fails unless one assumption is equal and exactly one is unifiable
   4.104 +**)
   4.105 +
   4.106 +ML {*
   4.107 +local
   4.108 +  fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P;
   4.109 +in
   4.110 +val uniq_assume_tac =
   4.111 +  SUBGOAL
   4.112 +    (fn (prem,i) =>
   4.113 +      let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
   4.114 +          and concl = discard_proof (Logic.strip_assums_concl prem)
   4.115 +      in
   4.116 +          if exists (fn hyp => hyp aconv concl) hyps
   4.117 +          then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
   4.118 +                   [_] => assume_tac i
   4.119 +                 |  _  => no_tac
   4.120 +          else no_tac
   4.121 +      end);
   4.122 +end;
   4.123 +*}
   4.124 +
   4.125 +
   4.126 +(*** Modus Ponens Tactics ***)
   4.127 +
   4.128 +(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   4.129 +ML {*
   4.130 +  fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac i
   4.131 +*}
   4.132 +
   4.133 +(*Like mp_tac but instantiates no variables*)
   4.134 +ML {*
   4.135 +  fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  uniq_assume_tac i
   4.136 +*}
   4.137 +
   4.138 +
   4.139 +(*** If-and-only-if ***)
   4.140 +
   4.141 +lemma iffI:
   4.142 +  assumes "!!x. x:P ==> q(x):Q"
   4.143 +    and "!!x. x:Q ==> r(x):P"
   4.144 +  shows "?p:P<->Q"
   4.145 +  unfolding iff_def
   4.146 +  apply (assumption | rule assms conjI impI)+
   4.147 +  done
   4.148 +
   4.149 +
   4.150 +(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   4.151 +  
   4.152 +lemma iffE:
   4.153 +  assumes "p:P <-> Q"
   4.154 +    and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
   4.155 +  shows "?p:R"
   4.156 +  apply (rule conjE)
   4.157 +   apply (rule assms(1) [unfolded iff_def])
   4.158 +  apply (rule assms(2))
   4.159 +   apply assumption+
   4.160 +  done
   4.161 +
   4.162 +(* Destruct rules for <-> similar to Modus Ponens *)
   4.163 +
   4.164 +lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
   4.165 +  unfolding iff_def
   4.166 +  apply (rule conjunct1 [THEN mp], assumption+)
   4.167 +  done
   4.168 +
   4.169 +lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
   4.170 +  unfolding iff_def
   4.171 +  apply (rule conjunct2 [THEN mp], assumption+)
   4.172 +  done
   4.173 +
   4.174 +lemma iff_refl: "?p:P <-> P"
   4.175 +  apply (rule iffI)
   4.176 +   apply assumption+
   4.177 +  done
   4.178 +
   4.179 +lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
   4.180 +  apply (erule iffE)
   4.181 +  apply (rule iffI)
   4.182 +   apply (erule (1) mp)+
   4.183 +  done
   4.184 +
   4.185 +lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
   4.186 +  apply (rule iffI)
   4.187 +   apply (assumption | erule iffE | erule (1) impE)+
   4.188 +  done
   4.189 +
   4.190 +(*** Unique existence.  NOTE THAT the following 2 quantifications
   4.191 +   EX!x such that [EX!y such that P(x,y)]     (sequential)
   4.192 +   EX!x,y such that P(x,y)                    (simultaneous)
   4.193 + do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   4.194 +***)
   4.195 +
   4.196 +lemma ex1I:
   4.197 +  assumes "p:P(a)"
   4.198 +    and "!!x u. u:P(x) ==> f(u) : x=a"
   4.199 +  shows "?p:EX! x. P(x)"
   4.200 +  unfolding ex1_def
   4.201 +  apply (assumption | rule assms exI conjI allI impI)+
   4.202 +  done
   4.203 +
   4.204 +lemma ex1E:
   4.205 +  assumes "p:EX! x. P(x)"
   4.206 +    and "!!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
   4.207 +  shows "?a : R"
   4.208 +  apply (insert assms(1) [unfolded ex1_def])
   4.209 +  apply (erule exE conjE | assumption | rule assms(1))+
   4.210 +  done
   4.211 +
   4.212 +
   4.213 +(*** <-> congruence rules for simplification ***)
   4.214 +
   4.215 +(*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
   4.216 +ML {*
   4.217 +fun iff_tac prems i =
   4.218 +    resolve_tac (prems RL [@{thm iffE}]) i THEN
   4.219 +    REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i)
   4.220 +*}
   4.221 +
   4.222 +lemma conj_cong:
   4.223 +  assumes "p:P <-> P'"
   4.224 +    and "!!x. x:P' ==> q(x):Q <-> Q'"
   4.225 +  shows "?p:(P&Q) <-> (P'&Q')"
   4.226 +  apply (insert assms(1))
   4.227 +  apply (assumption | rule iffI conjI |
   4.228 +    erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
   4.229 +  done
   4.230 +
   4.231 +lemma disj_cong:
   4.232 +  "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
   4.233 +  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
   4.234 +  done
   4.235 +
   4.236 +lemma imp_cong:
   4.237 +  assumes "p:P <-> P'"
   4.238 +    and "!!x. x:P' ==> q(x):Q <-> Q'"
   4.239 +  shows "?p:(P-->Q) <-> (P'-->Q')"
   4.240 +  apply (insert assms(1))
   4.241 +  apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} |
   4.242 +    tactic {* iff_tac @{thms assms} 1 *})+
   4.243 +  done
   4.244 +
   4.245 +lemma iff_cong:
   4.246 +  "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
   4.247 +  apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
   4.248 +  done
   4.249 +
   4.250 +lemma not_cong:
   4.251 +  "p:P <-> P' ==> ?p:~P <-> ~P'"
   4.252 +  apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
   4.253 +  done
   4.254 +
   4.255 +lemma all_cong:
   4.256 +  assumes "!!x. f(x):P(x) <-> Q(x)"
   4.257 +  shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
   4.258 +  apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
   4.259 +    tactic {* iff_tac @{thms assms} 1 *})+
   4.260 +  done
   4.261 +
   4.262 +lemma ex_cong:
   4.263 +  assumes "!!x. f(x):P(x) <-> Q(x)"
   4.264 +  shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
   4.265 +  apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
   4.266 +    tactic {* iff_tac @{thms assms} 1 *})+
   4.267 +  done
   4.268 +
   4.269 +(*NOT PROVED
   4.270 +bind_thm ("ex1_cong", prove_goal (the_context ())
   4.271 +    "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
   4.272 + (fn prems =>
   4.273 +  [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
   4.274 +      ORELSE   mp_tac 1
   4.275 +      ORELSE   iff_tac prems 1)) ]))
   4.276 +*)
   4.277 +
   4.278 +(*** Equality rules ***)
   4.279 +
   4.280 +lemmas refl = ieqI
   4.281 +
   4.282 +lemma subst:
   4.283 +  assumes prem1: "p:a=b"
   4.284 +    and prem2: "q:P(a)"
   4.285 +  shows "?p : P(b)"
   4.286 +  apply (rule prem2 [THEN rev_mp])
   4.287 +  apply (rule prem1 [THEN ieqE])
   4.288 +  apply (rule impI)
   4.289 +  apply assumption
   4.290 +  done
   4.291 +
   4.292 +lemma sym: "q:a=b ==> ?c:b=a"
   4.293 +  apply (erule subst)
   4.294 +  apply (rule refl)
   4.295 +  done
   4.296 +
   4.297 +lemma trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
   4.298 +  apply (erule (1) subst)
   4.299 +  done
   4.300 +
   4.301 +(** ~ b=a ==> ~ a=b **)
   4.302 +lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
   4.303 +  apply (erule contrapos)
   4.304 +  apply (erule sym)
   4.305 +  done
   4.306 +
   4.307 +(*calling "standard" reduces maxidx to 0*)
   4.308 +lemmas ssubst = sym [THEN subst, standard]
   4.309 +
   4.310 +(*A special case of ex1E that would otherwise need quantifier expansion*)
   4.311 +lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
   4.312 +  apply (erule ex1E)
   4.313 +  apply (rule trans)
   4.314 +   apply (rule_tac [2] sym)
   4.315 +   apply (assumption | erule spec [THEN mp])+
   4.316 +  done
   4.317 +
   4.318 +(** Polymorphic congruence rules **)
   4.319 +
   4.320 +lemma subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
   4.321 +  apply (erule ssubst)
   4.322 +  apply (rule refl)
   4.323 +  done
   4.324 +
   4.325 +lemma subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
   4.326 +  apply (erule ssubst)+
   4.327 +  apply (rule refl)
   4.328 +  done
   4.329 +
   4.330 +lemma subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
   4.331 +  apply (erule ssubst)+
   4.332 +  apply (rule refl)
   4.333 +  done
   4.334 +
   4.335 +(*Useful with eresolve_tac for proving equalties from known equalities.
   4.336 +        a = b
   4.337 +        |   |
   4.338 +        c = d   *)
   4.339 +lemma box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
   4.340 +  apply (rule trans)
   4.341 +   apply (rule trans)
   4.342 +    apply (rule sym)
   4.343 +    apply assumption+
   4.344 +  done
   4.345 +
   4.346 +(*Dual of box_equals: for proving equalities backwards*)
   4.347 +lemma simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
   4.348 +  apply (rule trans)
   4.349 +   apply (rule trans)
   4.350 +    apply (assumption | rule sym)+
   4.351 +  done
   4.352 +
   4.353 +(** Congruence rules for predicate letters **)
   4.354 +
   4.355 +lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
   4.356 +  apply (rule iffI)
   4.357 +   apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   4.358 +  done
   4.359 +
   4.360 +lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
   4.361 +  apply (rule iffI)
   4.362 +   apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   4.363 +  done
   4.364 +
   4.365 +lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
   4.366 +  apply (rule iffI)
   4.367 +   apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   4.368 +  done
   4.369 +
   4.370 +(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   4.371 +
   4.372 +ML_setup {*
   4.373 +  bind_thms ("pred_congs",
   4.374 +    flat (map (fn c =>
   4.375 +               map (fn th => read_instantiate [("P",c)] th)
   4.376 +                   [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
   4.377 +               (explode"PQRS")))
   4.378 +*}
   4.379 +
   4.380 +(*special case for the equality predicate!*)
   4.381 +lemmas eq_cong = pred2_cong [where P = "op =", standard]
   4.382 +
   4.383 +
   4.384 +(*** Simplifications of assumed implications.
   4.385 +     Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
   4.386 +     used with mp_tac (restricted to atomic formulae) is COMPLETE for
   4.387 +     intuitionistic propositional logic.  See
   4.388 +   R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   4.389 +    (preprint, University of St Andrews, 1991)  ***)
   4.390 +
   4.391 +lemma conj_impE:
   4.392 +  assumes major: "p:(P&Q)-->S"
   4.393 +    and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
   4.394 +  shows "?p:R"
   4.395 +  apply (assumption | rule conjI impI major [THEN mp] minor)+
   4.396 +  done
   4.397 +
   4.398 +lemma disj_impE:
   4.399 +  assumes major: "p:(P|Q)-->S"
   4.400 +    and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
   4.401 +  shows "?p:R"
   4.402 +  apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
   4.403 +      resolve_tac [@{thm disjI1}, @{thm disjI2}, @{thm impI},
   4.404 +        @{thm major} RS @{thm mp}, @{thm minor}] 1) *})
   4.405 +  done
   4.406 +
   4.407 +(*Simplifies the implication.  Classical version is stronger.
   4.408 +  Still UNSAFE since Q must be provable -- backtracking needed.  *)
   4.409 +lemma imp_impE:
   4.410 +  assumes major: "p:(P-->Q)-->S"
   4.411 +    and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
   4.412 +    and r2: "!!x. x:S ==> r(x):R"
   4.413 +  shows "?p:R"
   4.414 +  apply (assumption | rule impI major [THEN mp] r1 r2)+
   4.415 +  done
   4.416 +
   4.417 +(*Simplifies the implication.  Classical version is stronger.
   4.418 +  Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   4.419 +lemma not_impE:
   4.420 +  assumes major: "p:~P --> S"
   4.421 +    and r1: "!!y. y:P ==> q(y):False"
   4.422 +    and r2: "!!y. y:S ==> r(y):R"
   4.423 +  shows "?p:R"
   4.424 +  apply (assumption | rule notI impI major [THEN mp] r1 r2)+
   4.425 +  done
   4.426 +
   4.427 +(*Simplifies the implication.   UNSAFE.  *)
   4.428 +lemma iff_impE:
   4.429 +  assumes major: "p:(P<->Q)-->S"
   4.430 +    and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
   4.431 +    and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
   4.432 +    and r3: "!!x. x:S ==> s(x):R"
   4.433 +  shows "?p:R"
   4.434 +  apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
   4.435 +  done
   4.436 +
   4.437 +(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   4.438 +lemma all_impE:
   4.439 +  assumes major: "p:(ALL x. P(x))-->S"
   4.440 +    and r1: "!!x. q:P(x)"
   4.441 +    and r2: "!!y. y:S ==> r(y):R"
   4.442 +  shows "?p:R"
   4.443 +  apply (assumption | rule allI impI major [THEN mp] r1 r2)+
   4.444 +  done
   4.445 +
   4.446 +(*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   4.447 +lemma ex_impE:
   4.448 +  assumes major: "p:(EX x. P(x))-->S"
   4.449 +    and r: "!!y. y:P(a)-->S ==> q(y):R"
   4.450 +  shows "?p:R"
   4.451 +  apply (assumption | rule exI impI major [THEN mp] r)+
   4.452 +  done
   4.453 +
   4.454 +
   4.455 +lemma rev_cut_eq:
   4.456 +  assumes "p:a=b"
   4.457 +    and "!!x. x:a=b ==> f(x):R"
   4.458 +  shows "?p:R"
   4.459 +  apply (rule assms)+
   4.460 +  done
   4.461 +
   4.462 +lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
   4.463 +
   4.464 +use "hypsubst.ML"
   4.465 +
   4.466 +ML {*
   4.467 +
   4.468 +(*** Applying HypsubstFun to generate hyp_subst_tac ***)
   4.469 +
   4.470 +structure Hypsubst_Data =
   4.471 +struct
   4.472 +  (*Take apart an equality judgement; otherwise raise Match!*)
   4.473 +  fun dest_eq (Const (@{const_name Proof}, _) $
   4.474 +    (Const (@{const_name "op ="}, _)  $ t $ u) $ _) = (t, u);
   4.475 +
   4.476 +  val imp_intr = @{thm impI}
   4.477 +
   4.478 +  (*etac rev_cut_eq moves an equality to be the last premise. *)
   4.479 +  val rev_cut_eq = @{thm rev_cut_eq}
   4.480 +
   4.481 +  val rev_mp = @{thm rev_mp}
   4.482 +  val subst = @{thm subst}
   4.483 +  val sym = @{thm sym}
   4.484 +  val thin_refl = @{thm thin_refl}
   4.485 +end;
   4.486 +
   4.487 +structure Hypsubst = HypsubstFun(Hypsubst_Data);
   4.488 +open Hypsubst;
   4.489 +*}
   4.490 +
   4.491 +use "intprover.ML"
   4.492 +
   4.493 +
   4.494 +(*** Rewrite rules ***)
   4.495 +
   4.496 +lemma conj_rews:
   4.497 +  "?p1 : P & True <-> P"
   4.498 +  "?p2 : True & P <-> P"
   4.499 +  "?p3 : P & False <-> False"
   4.500 +  "?p4 : False & P <-> False"
   4.501 +  "?p5 : P & P <-> P"
   4.502 +  "?p6 : P & ~P <-> False"
   4.503 +  "?p7 : ~P & P <-> False"
   4.504 +  "?p8 : (P & Q) & R <-> P & (Q & R)"
   4.505 +  apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
   4.506 +  done
   4.507 +
   4.508 +lemma disj_rews:
   4.509 +  "?p1 : P | True <-> True"
   4.510 +  "?p2 : True | P <-> True"
   4.511 +  "?p3 : P | False <-> P"
   4.512 +  "?p4 : False | P <-> P"
   4.513 +  "?p5 : P | P <-> P"
   4.514 +  "?p6 : (P | Q) | R <-> P | (Q | R)"
   4.515 +  apply (tactic {* IntPr.fast_tac 1 *})+
   4.516 +  done
   4.517 +
   4.518 +lemma not_rews:
   4.519 +  "?p1 : ~ False <-> True"
   4.520 +  "?p2 : ~ True <-> False"
   4.521 +  apply (tactic {* IntPr.fast_tac 1 *})+
   4.522 +  done
   4.523 +
   4.524 +lemma imp_rews:
   4.525 +  "?p1 : (P --> False) <-> ~P"
   4.526 +  "?p2 : (P --> True) <-> True"
   4.527 +  "?p3 : (False --> P) <-> True"
   4.528 +  "?p4 : (True --> P) <-> P"
   4.529 +  "?p5 : (P --> P) <-> True"
   4.530 +  "?p6 : (P --> ~P) <-> ~P"
   4.531 +  apply (tactic {* IntPr.fast_tac 1 *})+
   4.532 +  done
   4.533 +
   4.534 +lemma iff_rews:
   4.535 +  "?p1 : (True <-> P) <-> P"
   4.536 +  "?p2 : (P <-> True) <-> P"
   4.537 +  "?p3 : (P <-> P) <-> True"
   4.538 +  "?p4 : (False <-> P) <-> ~P"
   4.539 +  "?p5 : (P <-> False) <-> ~P"
   4.540 +  apply (tactic {* IntPr.fast_tac 1 *})+
   4.541 +  done
   4.542 +
   4.543 +lemma quant_rews:
   4.544 +  "?p1 : (ALL x. P) <-> P"
   4.545 +  "?p2 : (EX x. P) <-> P"
   4.546 +  apply (tactic {* IntPr.fast_tac 1 *})+
   4.547 +  done
   4.548 +
   4.549 +(*These are NOT supplied by default!*)
   4.550 +lemma distrib_rews1:
   4.551 +  "?p1 : ~(P|Q) <-> ~P & ~Q"
   4.552 +  "?p2 : P & (Q | R) <-> P&Q | P&R"
   4.553 +  "?p3 : (Q | R) & P <-> Q&P | R&P"
   4.554 +  "?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)"
   4.555 +  apply (tactic {* IntPr.fast_tac 1 *})+
   4.556 +  done
   4.557 +
   4.558 +lemma distrib_rews2:
   4.559 +  "?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
   4.560 +  "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
   4.561 +  "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
   4.562 +  "?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"
   4.563 +  apply (tactic {* IntPr.fast_tac 1 *})+
   4.564 +  done
   4.565 +
   4.566 +lemmas distrib_rews = distrib_rews1 distrib_rews2
   4.567 +
   4.568 +lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
   4.569 +  apply (tactic {* IntPr.fast_tac 1 *})
   4.570 +  done
   4.571 +
   4.572 +lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
   4.573 +  apply (tactic {* IntPr.fast_tac 1 *})
   4.574 +  done
   4.575  
   4.576  end
   4.577 -
   4.578 -
     5.1 --- a/src/FOLP/IsaMakefile	Tue Mar 18 21:57:36 2008 +0100
     5.2 +++ b/src/FOLP/IsaMakefile	Tue Mar 18 22:19:18 2008 +0100
     5.3 @@ -26,7 +26,7 @@
     5.4  Pure:
     5.5  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
     5.6  
     5.7 -$(OUT)/FOLP: $(OUT)/Pure FOLP_lemmas.ML FOLP.thy IFOLP.ML IFOLP.thy ROOT.ML \
     5.8 +$(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML \
     5.9    classical.ML hypsubst.ML intprover.ML simp.ML simpdata.ML
    5.10  	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
    5.11  
    5.12 @@ -35,8 +35,9 @@
    5.13  
    5.14  FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
    5.15  
    5.16 -$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/Foundation.thy \
    5.17 -  ex/If.thy ex/int.ML ex/Intro.thy ex/Nat.thy \
    5.18 +$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/Foundation.thy \
    5.19 +  ex/If.thy ex/Intro.thy ex/Nat.thy ex/Intuitionistic.thy   \
    5.20 +  ex/Classical.thy					    \
    5.21    ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
    5.22  	@$(ISATOOL) usedir $(OUT)/FOLP ex
    5.23  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/FOLP/ex/Classical.thy	Tue Mar 18 22:19:18 2008 +0100
     6.3 @@ -0,0 +1,303 @@
     6.4 +(*  Title:      FOLP/ex/Classical.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 +    Copyright   1993  University of Cambridge
     6.8 +
     6.9 +Classical First-Order Logic.
    6.10 +*)
    6.11 +
    6.12 +theory Classical
    6.13 +imports FOLP
    6.14 +begin
    6.15 +
    6.16 +lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
    6.17 +  by (tactic "fast_tac FOLP_cs 1")
    6.18 +
    6.19 +(*If and only if*)
    6.20 +lemma "?p : (P<->Q) <-> (Q<->P)"
    6.21 +  by (tactic "fast_tac FOLP_cs 1")
    6.22 +
    6.23 +lemma "?p : ~ (P <-> ~P)"
    6.24 +  by (tactic "fast_tac FOLP_cs 1")
    6.25 +
    6.26 +
    6.27 +(*Sample problems from 
    6.28 +  F. J. Pelletier, 
    6.29 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
    6.30 +  J. Automated Reasoning 2 (1986), 191-216.
    6.31 +  Errata, JAR 4 (1988), 236-236.
    6.32 +
    6.33 +The hardest problems -- judging by experience with several theorem provers,
    6.34 +including matrix ones -- are 34 and 43.
    6.35 +*)
    6.36 +
    6.37 +text "Pelletier's examples"
    6.38 +(*1*)
    6.39 +lemma "?p : (P-->Q)  <->  (~Q --> ~P)"
    6.40 +  by (tactic "fast_tac FOLP_cs 1")
    6.41 +
    6.42 +(*2*)
    6.43 +lemma "?p : ~ ~ P  <->  P"
    6.44 +  by (tactic "fast_tac FOLP_cs 1")
    6.45 +
    6.46 +(*3*)
    6.47 +lemma "?p : ~(P-->Q) --> (Q-->P)"
    6.48 +  by (tactic "fast_tac FOLP_cs 1")
    6.49 +
    6.50 +(*4*)
    6.51 +lemma "?p : (~P-->Q)  <->  (~Q --> P)"
    6.52 +  by (tactic "fast_tac FOLP_cs 1")
    6.53 +
    6.54 +(*5*)
    6.55 +lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
    6.56 +  by (tactic "fast_tac FOLP_cs 1")
    6.57 +
    6.58 +(*6*)
    6.59 +lemma "?p : P | ~ P"
    6.60 +  by (tactic "fast_tac FOLP_cs 1")
    6.61 +
    6.62 +(*7*)
    6.63 +lemma "?p : P | ~ ~ ~ P"
    6.64 +  by (tactic "fast_tac FOLP_cs 1")
    6.65 +
    6.66 +(*8.  Peirce's law*)
    6.67 +lemma "?p : ((P-->Q) --> P)  -->  P"
    6.68 +  by (tactic "fast_tac FOLP_cs 1")
    6.69 +
    6.70 +(*9*)
    6.71 +lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
    6.72 +  by (tactic "fast_tac FOLP_cs 1")
    6.73 +
    6.74 +(*10*)
    6.75 +lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
    6.76 +  by (tactic "fast_tac FOLP_cs 1")
    6.77 +
    6.78 +(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
    6.79 +lemma "?p : P<->P"
    6.80 +  by (tactic "fast_tac FOLP_cs 1")
    6.81 +
    6.82 +(*12.  "Dijkstra's law"*)
    6.83 +lemma "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
    6.84 +  by (tactic "fast_tac FOLP_cs 1")
    6.85 +
    6.86 +(*13.  Distributive law*)
    6.87 +lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
    6.88 +  by (tactic "fast_tac FOLP_cs 1")
    6.89 +
    6.90 +(*14*)
    6.91 +lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
    6.92 +  by (tactic "fast_tac FOLP_cs 1")
    6.93 +
    6.94 +(*15*)
    6.95 +lemma "?p : (P --> Q) <-> (~P | Q)"
    6.96 +  by (tactic "fast_tac FOLP_cs 1")
    6.97 +
    6.98 +(*16*)
    6.99 +lemma "?p : (P-->Q) | (Q-->P)"
   6.100 +  by (tactic "fast_tac FOLP_cs 1")
   6.101 +
   6.102 +(*17*)
   6.103 +lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
   6.104 +  by (tactic "fast_tac FOLP_cs 1")
   6.105 +
   6.106 +
   6.107 +text "Classical Logic: examples with quantifiers"
   6.108 +
   6.109 +lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
   6.110 +  by (tactic "fast_tac FOLP_cs 1")
   6.111 +
   6.112 +lemma "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
   6.113 +  by (tactic "fast_tac FOLP_cs 1")
   6.114 +
   6.115 +lemma "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
   6.116 +  by (tactic "fast_tac FOLP_cs 1")
   6.117 +
   6.118 +lemma "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
   6.119 +  by (tactic "fast_tac FOLP_cs 1")
   6.120 +
   6.121 +
   6.122 +text "Problems requiring quantifier duplication"
   6.123 +
   6.124 +(*Needs multiple instantiation of ALL.*)
   6.125 +lemma "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
   6.126 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.127 +
   6.128 +(*Needs double instantiation of the quantifier*)
   6.129 +lemma "?p : EX x. P(x) --> P(a) & P(b)"
   6.130 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.131 +
   6.132 +lemma "?p : EX z. P(z) --> (ALL x. P(x))"
   6.133 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.134 +
   6.135 +
   6.136 +text "Hard examples with quantifiers"
   6.137 +
   6.138 +text "Problem 18"
   6.139 +lemma "?p : EX y. ALL x. P(y)-->P(x)"
   6.140 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.141 +
   6.142 +text "Problem 19"
   6.143 +lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
   6.144 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.145 +
   6.146 +text "Problem 20"
   6.147 +lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
   6.148 +    --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
   6.149 +  by (tactic "fast_tac FOLP_cs 1")
   6.150 +
   6.151 +text "Problem 21"
   6.152 +lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
   6.153 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.154 +
   6.155 +text "Problem 22"
   6.156 +lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
   6.157 +  by (tactic "fast_tac FOLP_cs 1")
   6.158 +
   6.159 +text "Problem 23"
   6.160 +lemma "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
   6.161 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.162 +
   6.163 +text "Problem 24"
   6.164 +lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
   6.165 +     (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
   6.166 +    --> (EX x. P(x)&R(x))"
   6.167 +  by (tactic "fast_tac FOLP_cs 1")
   6.168 +
   6.169 +text "Problem 25"
   6.170 +lemma "?p : (EX x. P(x)) &  
   6.171 +       (ALL x. L(x) --> ~ (M(x) & R(x))) &  
   6.172 +       (ALL x. P(x) --> (M(x) & L(x))) &   
   6.173 +       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  
   6.174 +   --> (EX x. Q(x)&P(x))"
   6.175 +  oops
   6.176 +
   6.177 +text "Problem 26"
   6.178 +lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
   6.179 +     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   
   6.180 +  --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
   6.181 +  by (tactic "fast_tac FOLP_cs 1")
   6.182 +
   6.183 +text "Problem 27"
   6.184 +lemma "?p : (EX x. P(x) & ~Q(x)) &    
   6.185 +              (ALL x. P(x) --> R(x)) &    
   6.186 +              (ALL x. M(x) & L(x) --> P(x)) &    
   6.187 +              ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))   
   6.188 +          --> (ALL x. M(x) --> ~L(x))"
   6.189 +  by (tactic "fast_tac FOLP_cs 1")
   6.190 +
   6.191 +text "Problem 28.  AMENDED"
   6.192 +lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &    
   6.193 +        ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &   
   6.194 +        ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))   
   6.195 +    --> (ALL x. P(x) & L(x) --> M(x))"
   6.196 +  by (tactic "fast_tac FOLP_cs 1")
   6.197 +
   6.198 +text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
   6.199 +lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
   6.200 +    --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
   6.201 +         (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
   6.202 +  by (tactic "fast_tac FOLP_cs 1")
   6.203 +
   6.204 +text "Problem 30"
   6.205 +lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &  
   6.206 +        (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
   6.207 +    --> (ALL x. S(x))"
   6.208 +  by (tactic "fast_tac FOLP_cs 1")
   6.209 +
   6.210 +text "Problem 31"
   6.211 +lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
   6.212 +        (EX x. L(x) & P(x)) &  
   6.213 +        (ALL x. ~ R(x) --> M(x))   
   6.214 +    --> (EX x. L(x) & M(x))"
   6.215 +  by (tactic "fast_tac FOLP_cs 1")
   6.216 +
   6.217 +text "Problem 32"
   6.218 +lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
   6.219 +        (ALL x. S(x) & R(x) --> L(x)) &  
   6.220 +        (ALL x. M(x) --> R(x))   
   6.221 +    --> (ALL x. P(x) & M(x) --> L(x))"
   6.222 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.223 +
   6.224 +text "Problem 33"
   6.225 +lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->     
   6.226 +     (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
   6.227 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.228 +
   6.229 +text "Problem 35"
   6.230 +lemma "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))"
   6.231 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.232 +
   6.233 +text "Problem 36"
   6.234 +lemma
   6.235 +"?p : (ALL x. EX y. J(x,y)) &  
   6.236 +      (ALL x. EX y. G(x,y)) &  
   6.237 +      (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))    
   6.238 +  --> (ALL x. EX y. H(x,y))"
   6.239 +  by (tactic "fast_tac FOLP_cs 1")
   6.240 +
   6.241 +text "Problem 37"
   6.242 +lemma "?p : (ALL z. EX w. ALL x. EX y.  
   6.243 +           (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &  
   6.244 +        (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &  
   6.245 +        ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))   
   6.246 +    --> (ALL x. EX y. R(x,y))"
   6.247 +  by (tactic "fast_tac FOLP_cs 1")
   6.248 +
   6.249 +text "Problem 39"
   6.250 +lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
   6.251 +  by (tactic "fast_tac FOLP_cs 1")
   6.252 +
   6.253 +text "Problem 40.  AMENDED"
   6.254 +lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
   6.255 +              ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
   6.256 +  by (tactic "fast_tac FOLP_cs 1")
   6.257 +
   6.258 +text "Problem 41"
   6.259 +lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))   
   6.260 +          --> ~ (EX z. ALL x. f(x,z))"
   6.261 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.262 +
   6.263 +text "Problem 44"
   6.264 +lemma "?p : (ALL x. f(x) -->                                     
   6.265 +              (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
   6.266 +              (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
   6.267 +              --> (EX x. j(x) & ~f(x))"
   6.268 +  by (tactic "fast_tac FOLP_cs 1")
   6.269 +
   6.270 +text "Problems (mainly) involving equality or functions"
   6.271 +
   6.272 +text "Problem 48"
   6.273 +lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
   6.274 +  by (tactic "fast_tac FOLP_cs 1")
   6.275 +
   6.276 +text "Problem 50"
   6.277 +(*What has this to do with equality?*)
   6.278 +lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
   6.279 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.280 +
   6.281 +text "Problem 56"
   6.282 +lemma
   6.283 + "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
   6.284 +  by (tactic "fast_tac FOLP_cs 1")
   6.285 +
   6.286 +text "Problem 57"
   6.287 +lemma
   6.288 +"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
   6.289 +      (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
   6.290 +  by (tactic "fast_tac FOLP_cs 1")
   6.291 +
   6.292 +text "Problem 58  NOT PROVED AUTOMATICALLY"
   6.293 +lemma
   6.294 +  notes f_cong = subst_context [where t = f]
   6.295 +  shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
   6.296 +  by (tactic {* fast_tac (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
   6.297 +
   6.298 +text "Problem 59"
   6.299 +lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
   6.300 +  by (tactic "best_tac FOLP_dup_cs 1")
   6.301 +
   6.302 +text "Problem 60"
   6.303 +lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
   6.304 +  by (tactic "fast_tac FOLP_cs 1")
   6.305 +
   6.306 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/FOLP/ex/Intuitionistic.thy	Tue Mar 18 22:19:18 2008 +0100
     7.3 @@ -0,0 +1,307 @@
     7.4 +(*  Title:      FOLP/ex/Intuitionistic.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +    Copyright   1991  University of Cambridge
     7.8 +
     7.9 +Intuitionistic First-Order Logic.
    7.10 +
    7.11 +Single-step commands:
    7.12 +by (IntPr.step_tac 1)
    7.13 +by (biresolve_tac safe_brls 1);
    7.14 +by (biresolve_tac haz_brls 1);
    7.15 +by (assume_tac 1);
    7.16 +by (IntPr.safe_tac 1);
    7.17 +by (IntPr.mp_tac 1);
    7.18 +by (IntPr.fast_tac 1);
    7.19 +*)
    7.20 +
    7.21 +(*Note: for PROPOSITIONAL formulae...
    7.22 +  ~A is classically provable iff it is intuitionistically provable.  
    7.23 +  Therefore A is classically provable iff ~~A is intuitionistically provable.
    7.24 +
    7.25 +Let Q be the conjuction of the propositions A|~A, one for each atom A in
    7.26 +P.  If P is provable classically, then clearly P&Q is provable
    7.27 +intuitionistically, so ~~(P&Q) is also provable intuitionistically.
    7.28 +The latter is intuitionistically equivalent to ~~P&~~Q, hence to ~~P,
    7.29 +since ~~Q is intuitionistically provable.  Finally, if P is a negation then
    7.30 +~~P is intuitionstically equivalent to P.  [Andy Pitts]
    7.31 +*)
    7.32 +
    7.33 +theory Intuitionistic
    7.34 +imports IFOLP
    7.35 +begin
    7.36 +
    7.37 +lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
    7.38 +  by (tactic {* IntPr.fast_tac 1 *})
    7.39 +
    7.40 +lemma "?p : ~~~P <-> ~P"
    7.41 +  by (tactic {* IntPr.fast_tac 1 *})
    7.42 +
    7.43 +lemma "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
    7.44 +  by (tactic {* IntPr.fast_tac 1 *})
    7.45 +
    7.46 +lemma "?p : (P<->Q) <-> (Q<->P)"
    7.47 +  by (tactic {* IntPr.fast_tac 1 *})
    7.48 +
    7.49 +
    7.50 +subsection {* Lemmas for the propositional double-negation translation *}
    7.51 +
    7.52 +lemma "?p : P --> ~~P"
    7.53 +  by (tactic {* IntPr.fast_tac 1 *})
    7.54 +
    7.55 +lemma "?p : ~~(~~P --> P)"
    7.56 +  by (tactic {* IntPr.fast_tac 1 *})
    7.57 +
    7.58 +lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
    7.59 +  by (tactic {* IntPr.fast_tac 1 *})
    7.60 +
    7.61 +
    7.62 +subsection {* The following are classically but not constructively valid *}
    7.63 +
    7.64 +(*The attempt to prove them terminates quickly!*)
    7.65 +lemma "?p : ((P-->Q) --> P)  -->  P"
    7.66 +  apply (tactic {* IntPr.fast_tac 1 *})?
    7.67 +  oops
    7.68 +
    7.69 +lemma "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)"
    7.70 +  apply (tactic {* IntPr.fast_tac 1 *})?
    7.71 +  oops
    7.72 +
    7.73 +
    7.74 +subsection {* Intuitionistic FOL: propositional problems based on Pelletier *}
    7.75 +
    7.76 +text "Problem ~~1"
    7.77 +lemma "?p : ~~((P-->Q)  <->  (~Q --> ~P))"
    7.78 +  by (tactic {* IntPr.fast_tac 1 *})
    7.79 +
    7.80 +text "Problem ~~2"
    7.81 +lemma "?p : ~~(~~P  <->  P)"
    7.82 +  by (tactic {* IntPr.fast_tac 1 *})
    7.83 +
    7.84 +text "Problem 3"
    7.85 +lemma "?p : ~(P-->Q) --> (Q-->P)"
    7.86 +  by (tactic {* IntPr.fast_tac 1 *})
    7.87 +
    7.88 +text "Problem ~~4"
    7.89 +lemma "?p : ~~((~P-->Q)  <->  (~Q --> P))"
    7.90 +  by (tactic {* IntPr.fast_tac 1 *})
    7.91 +
    7.92 +text "Problem ~~5"
    7.93 +lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
    7.94 +  by (tactic {* IntPr.fast_tac 1 *})
    7.95 +
    7.96 +text "Problem ~~6"
    7.97 +lemma "?p : ~~(P | ~P)"
    7.98 +  by (tactic {* IntPr.fast_tac 1 *})
    7.99 +
   7.100 +text "Problem ~~7"
   7.101 +lemma "?p : ~~(P | ~~~P)"
   7.102 +  by (tactic {* IntPr.fast_tac 1 *})
   7.103 +
   7.104 +text "Problem ~~8.  Peirce's law"
   7.105 +lemma "?p : ~~(((P-->Q) --> P)  -->  P)"
   7.106 +  by (tactic {* IntPr.fast_tac 1 *})
   7.107 +
   7.108 +text "Problem 9"
   7.109 +lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   7.110 +  by (tactic {* IntPr.fast_tac 1 *})
   7.111 +
   7.112 +text "Problem 10"
   7.113 +lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
   7.114 +  by (tactic {* IntPr.fast_tac 1 *})
   7.115 +
   7.116 +text "11.  Proved in each direction (incorrectly, says Pelletier!!) "
   7.117 +lemma "?p : P<->P"
   7.118 +  by (tactic {* IntPr.fast_tac 1 *})
   7.119 +
   7.120 +text "Problem ~~12.  Dijkstra's law  "
   7.121 +lemma "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
   7.122 +  by (tactic {* IntPr.fast_tac 1 *})
   7.123 +
   7.124 +lemma "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
   7.125 +  by (tactic {* IntPr.fast_tac 1 *})
   7.126 +
   7.127 +text "Problem 13.  Distributive law"
   7.128 +lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
   7.129 +  by (tactic {* IntPr.fast_tac 1 *})
   7.130 +
   7.131 +text "Problem ~~14"
   7.132 +lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
   7.133 +  by (tactic {* IntPr.fast_tac 1 *})
   7.134 +
   7.135 +text "Problem ~~15"
   7.136 +lemma "?p : ~~((P --> Q) <-> (~P | Q))"
   7.137 +  by (tactic {* IntPr.fast_tac 1 *})
   7.138 +
   7.139 +text "Problem ~~16"
   7.140 +lemma "?p : ~~((P-->Q) | (Q-->P))"
   7.141 +  by (tactic {* IntPr.fast_tac 1 *})
   7.142 +
   7.143 +text "Problem ~~17"
   7.144 +lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
   7.145 +  by (tactic {* IntPr.fast_tac 1 *})  -- slow
   7.146 +
   7.147 +
   7.148 +subsection {* Examples with quantifiers *}
   7.149 +
   7.150 +text "The converse is classical in the following implications..."
   7.151 +
   7.152 +lemma "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
   7.153 +  by (tactic {* IntPr.fast_tac 1 *})
   7.154 +
   7.155 +lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
   7.156 +  by (tactic {* IntPr.fast_tac 1 *})
   7.157 +
   7.158 +lemma "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
   7.159 +  by (tactic {* IntPr.fast_tac 1 *})
   7.160 +
   7.161 +lemma "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
   7.162 +  by (tactic {* IntPr.fast_tac 1 *})
   7.163 +
   7.164 +lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
   7.165 +  by (tactic {* IntPr.fast_tac 1 *})
   7.166 +
   7.167 +
   7.168 +text "The following are not constructively valid!"
   7.169 +text "The attempt to prove them terminates quickly!"
   7.170 +
   7.171 +lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
   7.172 +  apply (tactic {* IntPr.fast_tac 1 *})?
   7.173 +  oops
   7.174 +
   7.175 +lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
   7.176 +  apply (tactic {* IntPr.fast_tac 1 *})?
   7.177 +  oops
   7.178 +
   7.179 +lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
   7.180 +  apply (tactic {* IntPr.fast_tac 1 *})?
   7.181 +  oops
   7.182 +
   7.183 +lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
   7.184 +  apply (tactic {* IntPr.fast_tac 1 *})?
   7.185 +  oops
   7.186 +
   7.187 +(*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
   7.188 +lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
   7.189 +  apply (tactic {* IntPr.fast_tac 1 *})?
   7.190 +  oops
   7.191 +
   7.192 +
   7.193 +subsection "Hard examples with quantifiers"
   7.194 +
   7.195 +text {*
   7.196 +  The ones that have not been proved are not known to be valid!
   7.197 +  Some will require quantifier duplication -- not currently available.
   7.198 +*}
   7.199 +
   7.200 +text "Problem ~~18"
   7.201 +lemma "?p : ~~(EX y. ALL x. P(y)-->P(x))" oops
   7.202 +(*NOT PROVED*)
   7.203 +
   7.204 +text "Problem ~~19"
   7.205 +lemma "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))" oops
   7.206 +(*NOT PROVED*)
   7.207 +
   7.208 +text "Problem 20"
   7.209 +lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
   7.210 +    --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
   7.211 +  by (tactic {* IntPr.fast_tac 1 *})
   7.212 +
   7.213 +text "Problem 21"
   7.214 +lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
   7.215 +(*NOT PROVED*)
   7.216 +
   7.217 +text "Problem 22"
   7.218 +lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
   7.219 +  by (tactic {* IntPr.fast_tac 1 *})
   7.220 +
   7.221 +text "Problem ~~23"
   7.222 +lemma "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
   7.223 +  by (tactic {* IntPr.fast_tac 1 *})
   7.224 +
   7.225 +text "Problem 24"
   7.226 +lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
   7.227 +     (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
   7.228 +    --> ~~(EX x. P(x)&R(x))"
   7.229 +(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
   7.230 +  apply (tactic "IntPr.safe_tac")
   7.231 +  apply (erule impE)
   7.232 +   apply (tactic "IntPr.fast_tac 1")
   7.233 +  apply (tactic "IntPr.fast_tac 1")
   7.234 +  done
   7.235 +
   7.236 +text "Problem 25"
   7.237 +lemma "?p : (EX x. P(x)) &   
   7.238 +        (ALL x. L(x) --> ~ (M(x) & R(x))) &   
   7.239 +        (ALL x. P(x) --> (M(x) & L(x))) &    
   7.240 +        ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))   
   7.241 +    --> (EX x. Q(x)&P(x))"
   7.242 +  by (tactic "IntPr.best_tac 1")
   7.243 +
   7.244 +text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
   7.245 +lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
   7.246 +    --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
   7.247 +         (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
   7.248 +  by (tactic "IntPr.fast_tac 1")
   7.249 +
   7.250 +text "Problem ~~30"
   7.251 +lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &  
   7.252 +        (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
   7.253 +    --> (ALL x. ~~S(x))"
   7.254 +  by (tactic "IntPr.fast_tac 1")
   7.255 +
   7.256 +text "Problem 31"
   7.257 +lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
   7.258 +        (EX x. L(x) & P(x)) &  
   7.259 +        (ALL x. ~ R(x) --> M(x))   
   7.260 +    --> (EX x. L(x) & M(x))"
   7.261 +  by (tactic "IntPr.fast_tac 1")
   7.262 +
   7.263 +text "Problem 32"
   7.264 +lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
   7.265 +        (ALL x. S(x) & R(x) --> L(x)) &  
   7.266 +        (ALL x. M(x) --> R(x))   
   7.267 +    --> (ALL x. P(x) & M(x) --> L(x))"
   7.268 +  by (tactic "IntPr.best_tac 1") -- slow
   7.269 +
   7.270 +text "Problem 39"
   7.271 +lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
   7.272 +  by (tactic "IntPr.best_tac 1")
   7.273 +
   7.274 +text "Problem 40.  AMENDED"
   7.275 +lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
   7.276 +              ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
   7.277 +  by (tactic "IntPr.best_tac 1") -- slow
   7.278 +
   7.279 +text "Problem 44"
   7.280 +lemma "?p : (ALL x. f(x) -->                                    
   7.281 +              (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
   7.282 +              (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
   7.283 +              --> (EX x. j(x) & ~f(x))"
   7.284 +  by (tactic "IntPr.best_tac 1")
   7.285 +
   7.286 +text "Problem 48"
   7.287 +lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
   7.288 +  by (tactic "IntPr.best_tac 1")
   7.289 +
   7.290 +text "Problem 51"
   7.291 +lemma
   7.292 +    "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
   7.293 +     (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
   7.294 +  by (tactic "IntPr.best_tac 1") -- {*60 seconds*}
   7.295 +
   7.296 +text "Problem 56"
   7.297 +lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
   7.298 +  by (tactic "IntPr.best_tac 1")
   7.299 +
   7.300 +text "Problem 57"
   7.301 +lemma
   7.302 +    "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
   7.303 +     (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
   7.304 +  by (tactic "IntPr.best_tac 1")
   7.305 +
   7.306 +text "Problem 60"
   7.307 +lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
   7.308 +  by (tactic "IntPr.best_tac 1")
   7.309 +
   7.310 +end
     8.1 --- a/src/FOLP/ex/ROOT.ML	Tue Mar 18 21:57:36 2008 +0100
     8.2 +++ b/src/FOLP/ex/ROOT.ML	Tue Mar 18 22:19:18 2008 +0100
     8.3 @@ -10,19 +10,15 @@
     8.4    "Intro",
     8.5    "Nat",
     8.6    "Foundation",
     8.7 -  "If"
     8.8 +  "If",
     8.9 +  "Intuitionistic",
    8.10 +  "Classical"
    8.11  ];
    8.12  
    8.13 -writeln"\n** Intuitionistic examples **\n";
    8.14 -time_use     "int.ML";
    8.15 -
    8.16  val thy = theory "IFOLP"  and  tac = IntPr.fast_tac 1;
    8.17  time_use     "prop.ML";
    8.18  time_use     "quant.ML";
    8.19  
    8.20 -writeln"\n** Classical examples **\n";
    8.21 -time_use     "cla.ML";
    8.22 -
    8.23  val thy = theory "FOLP"  and  tac = Cla.fast_tac FOLP_cs 1;
    8.24  time_use     "prop.ML";
    8.25  time_use     "quant.ML";
     9.1 --- a/src/FOLP/ex/cla.ML	Tue Mar 18 21:57:36 2008 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,354 +0,0 @@
     9.4 -(*  Title:      FOLP/ex/cla
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1993  University of Cambridge
     9.8 -
     9.9 -Classical First-Order Logic.
    9.10 -*)
    9.11 -
    9.12 -goal (theory "FOLP") "?p : (P --> Q | R) --> (P-->Q) | (P-->R)";
    9.13 -by (fast_tac FOLP_cs 1);
    9.14 -result();
    9.15 -
    9.16 -(*If and only if*)
    9.17 -
    9.18 -goal (theory "FOLP") "?p : (P<->Q) <-> (Q<->P)";
    9.19 -by (fast_tac FOLP_cs 1);
    9.20 -result();
    9.21 -
    9.22 -goal (theory "FOLP") "?p : ~ (P <-> ~P)";
    9.23 -by (fast_tac FOLP_cs 1);
    9.24 -result();
    9.25 -
    9.26 -
    9.27 -(*Sample problems from 
    9.28 -  F. J. Pelletier, 
    9.29 -  Seventy-Five Problems for Testing Automatic Theorem Provers,
    9.30 -  J. Automated Reasoning 2 (1986), 191-216.
    9.31 -  Errata, JAR 4 (1988), 236-236.
    9.32 -
    9.33 -The hardest problems -- judging by experience with several theorem provers,
    9.34 -including matrix ones -- are 34 and 43.
    9.35 -*)
    9.36 -
    9.37 -writeln"Pelletier's examples";
    9.38 -(*1*)
    9.39 -goal (theory "FOLP") "?p : (P-->Q)  <->  (~Q --> ~P)";
    9.40 -by (fast_tac FOLP_cs 1);
    9.41 -result();
    9.42 -
    9.43 -(*2*)
    9.44 -goal (theory "FOLP") "?p : ~ ~ P  <->  P";
    9.45 -by (fast_tac FOLP_cs 1);
    9.46 -result();
    9.47 -
    9.48 -(*3*)
    9.49 -goal (theory "FOLP") "?p : ~(P-->Q) --> (Q-->P)";
    9.50 -by (fast_tac FOLP_cs 1);
    9.51 -result();
    9.52 -
    9.53 -(*4*)
    9.54 -goal (theory "FOLP") "?p : (~P-->Q)  <->  (~Q --> P)";
    9.55 -by (fast_tac FOLP_cs 1);
    9.56 -result();
    9.57 -
    9.58 -(*5*)
    9.59 -goal (theory "FOLP") "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))";
    9.60 -by (fast_tac FOLP_cs 1);
    9.61 -result();
    9.62 -
    9.63 -(*6*)
    9.64 -goal (theory "FOLP") "?p : P | ~ P";
    9.65 -by (fast_tac FOLP_cs 1);
    9.66 -result();
    9.67 -
    9.68 -(*7*)
    9.69 -goal (theory "FOLP") "?p : P | ~ ~ ~ P";
    9.70 -by (fast_tac FOLP_cs 1);
    9.71 -result();
    9.72 -
    9.73 -(*8.  Peirce's law*)
    9.74 -goal (theory "FOLP") "?p : ((P-->Q) --> P)  -->  P";
    9.75 -by (fast_tac FOLP_cs 1);
    9.76 -result();
    9.77 -
    9.78 -(*9*)
    9.79 -goal (theory "FOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
    9.80 -by (fast_tac FOLP_cs 1);
    9.81 -result();
    9.82 -
    9.83 -(*10*)
    9.84 -goal (theory "FOLP") "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";
    9.85 -by (fast_tac FOLP_cs 1);
    9.86 -result();
    9.87 -
    9.88 -(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
    9.89 -goal (theory "FOLP") "?p : P<->P";
    9.90 -by (fast_tac FOLP_cs 1);
    9.91 -result();
    9.92 -
    9.93 -(*12.  "Dijkstra's law"*)
    9.94 -goal (theory "FOLP") "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
    9.95 -by (fast_tac FOLP_cs 1);
    9.96 -result();
    9.97 -
    9.98 -(*13.  Distributive law*)
    9.99 -goal (theory "FOLP") "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
   9.100 -by (fast_tac FOLP_cs 1);
   9.101 -result();
   9.102 -
   9.103 -(*14*)
   9.104 -goal (theory "FOLP") "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
   9.105 -by (fast_tac FOLP_cs 1);
   9.106 -result();
   9.107 -
   9.108 -(*15*)
   9.109 -goal (theory "FOLP") "?p : (P --> Q) <-> (~P | Q)";
   9.110 -by (fast_tac FOLP_cs 1);
   9.111 -result();
   9.112 -
   9.113 -(*16*)
   9.114 -goal (theory "FOLP") "?p : (P-->Q) | (Q-->P)";
   9.115 -by (fast_tac FOLP_cs 1);
   9.116 -result();
   9.117 -
   9.118 -(*17*)
   9.119 -goal (theory "FOLP") "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
   9.120 -by (fast_tac FOLP_cs 1);
   9.121 -result();
   9.122 -
   9.123 -writeln"Classical Logic: examples with quantifiers";
   9.124 -
   9.125 -goal (theory "FOLP") "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
   9.126 -by (fast_tac FOLP_cs 1);
   9.127 -result(); 
   9.128 -
   9.129 -goal (theory "FOLP") "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   9.130 -by (fast_tac FOLP_cs 1);
   9.131 -result(); 
   9.132 -
   9.133 -goal (theory "FOLP") "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
   9.134 -by (fast_tac FOLP_cs 1);
   9.135 -result(); 
   9.136 -
   9.137 -goal (theory "FOLP") "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
   9.138 -by (fast_tac FOLP_cs 1);
   9.139 -result(); 
   9.140 -
   9.141 -writeln"Problems requiring quantifier duplication";
   9.142 -
   9.143 -(*Needs multiple instantiation of ALL.*)
   9.144 -(*
   9.145 -goal (theory "FOLP") "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
   9.146 -by (best_tac FOLP_dup_cs 1);
   9.147 -result();
   9.148 -*)
   9.149 -(*Needs double instantiation of the quantifier*)
   9.150 -goal (theory "FOLP") "?p : EX x. P(x) --> P(a) & P(b)";
   9.151 -by (best_tac FOLP_dup_cs 1);
   9.152 -result();
   9.153 -
   9.154 -goal (theory "FOLP") "?p : EX z. P(z) --> (ALL x. P(x))";
   9.155 -by (best_tac FOLP_dup_cs 1);
   9.156 -result();
   9.157 -
   9.158 -
   9.159 -writeln"Hard examples with quantifiers";
   9.160 -
   9.161 -writeln"Problem 18";
   9.162 -goal (theory "FOLP") "?p : EX y. ALL x. P(y)-->P(x)";
   9.163 -by (best_tac FOLP_dup_cs 1);
   9.164 -result(); 
   9.165 -
   9.166 -writeln"Problem 19";
   9.167 -goal (theory "FOLP") "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
   9.168 -by (best_tac FOLP_dup_cs 1);
   9.169 -result();
   9.170 -
   9.171 -writeln"Problem 20";
   9.172 -goal (theory "FOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
   9.173 -\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
   9.174 -by (fast_tac FOLP_cs 1); 
   9.175 -result();
   9.176 -(*
   9.177 -writeln"Problem 21";
   9.178 -goal (theory "FOLP") "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
   9.179 -by (best_tac FOLP_dup_cs 1);
   9.180 -result();
   9.181 -*)
   9.182 -writeln"Problem 22";
   9.183 -goal (theory "FOLP") "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
   9.184 -by (fast_tac FOLP_cs 1); 
   9.185 -result();
   9.186 -
   9.187 -writeln"Problem 23";
   9.188 -goal (theory "FOLP") "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
   9.189 -by (best_tac FOLP_cs 1);  
   9.190 -result();
   9.191 -
   9.192 -writeln"Problem 24";
   9.193 -goal (theory "FOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
   9.194 -\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
   9.195 -\   --> (EX x. P(x)&R(x))";
   9.196 -by (fast_tac FOLP_cs 1); 
   9.197 -result();
   9.198 -(*
   9.199 -writeln"Problem 25";
   9.200 -goal (theory "FOLP") "?p : (EX x. P(x)) &  \
   9.201 -\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
   9.202 -\       (ALL x. P(x) --> (M(x) & L(x))) &   \
   9.203 -\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
   9.204 -\   --> (EX x. Q(x)&P(x))";
   9.205 -by (best_tac FOLP_cs 1); 
   9.206 -result();
   9.207 -
   9.208 -writeln"Problem 26";
   9.209 -goal (theory "FOLP") "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   \
   9.210 -\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
   9.211 -\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
   9.212 -by (fast_tac FOLP_cs 1);
   9.213 -result();
   9.214 -*)
   9.215 -writeln"Problem 27";
   9.216 -goal (theory "FOLP") "?p : (EX x. P(x) & ~Q(x)) &   \
   9.217 -\             (ALL x. P(x) --> R(x)) &   \
   9.218 -\             (ALL x. M(x) & L(x) --> P(x)) &   \
   9.219 -\             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
   9.220 -\         --> (ALL x. M(x) --> ~L(x))";
   9.221 -by (fast_tac FOLP_cs 1); 
   9.222 -result();
   9.223 -
   9.224 -writeln"Problem 28.  AMENDED";
   9.225 -goal (theory "FOLP") "?p : (ALL x. P(x) --> (ALL x. Q(x))) &   \
   9.226 -\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
   9.227 -\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
   9.228 -\   --> (ALL x. P(x) & L(x) --> M(x))";
   9.229 -by (fast_tac FOLP_cs 1);  
   9.230 -result();
   9.231 -
   9.232 -writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   9.233 -goal (theory "FOLP") "?p : (EX x. P(x)) & (EX y. Q(y))  \
   9.234 -\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
   9.235 -\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
   9.236 -by (fast_tac FOLP_cs 1); 
   9.237 -result();
   9.238 -
   9.239 -writeln"Problem 30";
   9.240 -goal (theory "FOLP") "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) & \
   9.241 -\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
   9.242 -\   --> (ALL x. S(x))";
   9.243 -by (fast_tac FOLP_cs 1);  
   9.244 -result();
   9.245 -
   9.246 -writeln"Problem 31";
   9.247 -goal (theory "FOLP") "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
   9.248 -\       (EX x. L(x) & P(x)) & \
   9.249 -\       (ALL x. ~ R(x) --> M(x))  \
   9.250 -\   --> (EX x. L(x) & M(x))";
   9.251 -by (fast_tac FOLP_cs 1);
   9.252 -result();
   9.253 -
   9.254 -writeln"Problem 32";
   9.255 -goal (theory "FOLP") "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
   9.256 -\       (ALL x. S(x) & R(x) --> L(x)) & \
   9.257 -\       (ALL x. M(x) --> R(x))  \
   9.258 -\   --> (ALL x. P(x) & M(x) --> L(x))";
   9.259 -by (best_tac FOLP_cs 1);
   9.260 -result();
   9.261 -
   9.262 -writeln"Problem 33";
   9.263 -goal (theory "FOLP") "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
   9.264 -\    (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
   9.265 -by (best_tac FOLP_cs 1);
   9.266 -result();
   9.267 -
   9.268 -writeln"Problem 35";
   9.269 -goal (theory "FOLP") "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))";
   9.270 -by (best_tac FOLP_dup_cs 1);
   9.271 -result();
   9.272 -
   9.273 -writeln"Problem 36";
   9.274 -goal (theory "FOLP")
   9.275 -"?p : (ALL x. EX y. J(x,y)) & \
   9.276 -\     (ALL x. EX y. G(x,y)) & \
   9.277 -\     (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
   9.278 -\ --> (ALL x. EX y. H(x,y))";
   9.279 -by (fast_tac FOLP_cs 1);
   9.280 -result();
   9.281 -
   9.282 -writeln"Problem 37";
   9.283 -goal (theory "FOLP") "?p : (ALL z. EX w. ALL x. EX y. \
   9.284 -\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
   9.285 -\       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
   9.286 -\       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
   9.287 -\   --> (ALL x. EX y. R(x,y))";
   9.288 -by (fast_tac FOLP_cs 1);
   9.289 -result();
   9.290 -
   9.291 -writeln"Problem 39";
   9.292 -goal (theory "FOLP") "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
   9.293 -by (fast_tac FOLP_cs 1);
   9.294 -result();
   9.295 -
   9.296 -writeln"Problem 40.  AMENDED";
   9.297 -goal (theory "FOLP") "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
   9.298 -\             ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
   9.299 -by (fast_tac FOLP_cs 1);
   9.300 -result();
   9.301 -
   9.302 -writeln"Problem 41";
   9.303 -goal (theory "FOLP") "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))  \
   9.304 -\         --> ~ (EX z. ALL x. f(x,z))";
   9.305 -by (best_tac FOLP_cs 1);
   9.306 -result();
   9.307 -
   9.308 -writeln"Problem 44";
   9.309 -goal (theory "FOLP") "?p : (ALL x. f(x) -->                                    \
   9.310 -\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
   9.311 -\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
   9.312 -\             --> (EX x. j(x) & ~f(x))";
   9.313 -by (fast_tac FOLP_cs 1);
   9.314 -result();
   9.315 -
   9.316 -writeln"Problems (mainly) involving equality or functions";
   9.317 -
   9.318 -writeln"Problem 48";
   9.319 -goal (theory "FOLP") "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
   9.320 -by (fast_tac FOLP_cs 1);
   9.321 -result();
   9.322 -
   9.323 -writeln"Problem 50";  
   9.324 -(*What has this to do with equality?*)
   9.325 -goal (theory "FOLP") "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
   9.326 -by (best_tac FOLP_dup_cs 1);
   9.327 -result();
   9.328 -
   9.329 -writeln"Problem 56";
   9.330 -goal (theory "FOLP")
   9.331 - "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
   9.332 -by (fast_tac FOLP_cs 1);
   9.333 -result();
   9.334 -
   9.335 -writeln"Problem 57";
   9.336 -goal (theory "FOLP")
   9.337 -"?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
   9.338 -\     (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
   9.339 -by (fast_tac FOLP_cs 1);
   9.340 -result();
   9.341 -
   9.342 -writeln"Problem 58  NOT PROVED AUTOMATICALLY";
   9.343 -goal (theory "FOLP") "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
   9.344 -val f_cong = read_instantiate [("t","f")] subst_context;
   9.345 -by (fast_tac (FOLP_cs addIs [f_cong]) 1);
   9.346 -result();
   9.347 -
   9.348 -writeln"Problem 59";
   9.349 -goal (theory "FOLP") "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
   9.350 -by (best_tac FOLP_dup_cs 1);
   9.351 -result();
   9.352 -
   9.353 -writeln"Problem 60";
   9.354 -goal (theory "FOLP")
   9.355 -"?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
   9.356 -by (fast_tac FOLP_cs 1);
   9.357 -result();
    10.1 --- a/src/FOLP/ex/int.ML	Tue Mar 18 21:57:36 2008 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,361 +0,0 @@
    10.4 -(*  Title:      FOLP/ex/int.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 -    Copyright   1991  University of Cambridge
    10.8 -
    10.9 -Intuitionistic First-Order Logic
   10.10 -
   10.11 -Single-step commands:
   10.12 -by (IntPr.step_tac 1);
   10.13 -by (biresolve_tac safe_brls 1);
   10.14 -by (biresolve_tac haz_brls 1);
   10.15 -by (assume_tac 1);
   10.16 -by (IntPr.safe_tac 1);
   10.17 -by (IntPr.mp_tac 1);
   10.18 -by (IntPr.fast_tac 1);
   10.19 -*)
   10.20 -
   10.21 -(*Note: for PROPOSITIONAL formulae...
   10.22 -  ~A is classically provable iff it is intuitionistically provable.  
   10.23 -  Therefore A is classically provable iff ~~A is intuitionistically provable.
   10.24 -
   10.25 -Let Q be the conjuction of the propositions A|~A, one for each atom A in
   10.26 -P.  If P is provable classically, then clearly P&Q is provable
   10.27 -intuitionistically, so ~~(P&Q) is also provable intuitionistically.
   10.28 -The latter is intuitionistically equivalent to ~~P&~~Q, hence to ~~P,
   10.29 -since ~~Q is intuitionistically provable.  Finally, if P is a negation then
   10.30 -~~P is intuitionstically equivalent to P.  [Andy Pitts]
   10.31 -*)
   10.32 -
   10.33 -goal (theory "IFOLP") "?p : ~~(P&Q) <-> ~~P & ~~Q";
   10.34 -by (IntPr.fast_tac 1);
   10.35 -result();
   10.36 -
   10.37 -goal (theory "IFOLP") "?p : ~~~P <-> ~P";
   10.38 -by (IntPr.fast_tac 1);
   10.39 -result();
   10.40 -
   10.41 -goal (theory "IFOLP") "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))";
   10.42 -by (IntPr.fast_tac 1);
   10.43 -result();
   10.44 -
   10.45 -goal (theory "IFOLP") "?p : (P<->Q) <-> (Q<->P)";
   10.46 -by (IntPr.fast_tac 1);
   10.47 -result();
   10.48 -
   10.49 -
   10.50 -writeln"Lemmas for the propositional double-negation translation";
   10.51 -
   10.52 -goal (theory "IFOLP") "?p : P --> ~~P";
   10.53 -by (IntPr.fast_tac 1);
   10.54 -result();
   10.55 -
   10.56 -goal (theory "IFOLP") "?p : ~~(~~P --> P)";
   10.57 -by (IntPr.fast_tac 1);
   10.58 -result();
   10.59 -
   10.60 -goal (theory "IFOLP") "?p : ~~P & ~~(P --> Q) --> ~~Q";
   10.61 -by (IntPr.fast_tac 1);
   10.62 -result();
   10.63 -
   10.64 -
   10.65 -writeln"The following are classically but not constructively valid.";
   10.66 -
   10.67 -(*The attempt to prove them terminates quickly!*)
   10.68 -goal (theory "IFOLP") "?p : ((P-->Q) --> P)  -->  P";
   10.69 -by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
   10.70 -(*Check that subgoals remain: proof failed.*)
   10.71 -getgoal 1;  
   10.72 -
   10.73 -goal (theory "IFOLP") "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)";
   10.74 -by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
   10.75 -getgoal 1;  
   10.76 -
   10.77 -
   10.78 -writeln"Intuitionistic FOL: propositional problems based on Pelletier.";
   10.79 -
   10.80 -writeln"Problem ~~1";
   10.81 -goal (theory "IFOLP") "?p : ~~((P-->Q)  <->  (~Q --> ~P))";
   10.82 -by (IntPr.fast_tac 1);
   10.83 -result();
   10.84 -(*5 secs*)
   10.85 -
   10.86 -
   10.87 -writeln"Problem ~~2";
   10.88 -goal (theory "IFOLP") "?p : ~~(~~P  <->  P)";
   10.89 -by (IntPr.fast_tac 1);
   10.90 -result();
   10.91 -(*1 secs*)
   10.92 -
   10.93 -
   10.94 -writeln"Problem 3";
   10.95 -goal (theory "IFOLP") "?p : ~(P-->Q) --> (Q-->P)";
   10.96 -by (IntPr.fast_tac 1);
   10.97 -result();
   10.98 -
   10.99 -writeln"Problem ~~4";
  10.100 -goal (theory "IFOLP") "?p : ~~((~P-->Q)  <->  (~Q --> P))";
  10.101 -by (IntPr.fast_tac 1);
  10.102 -result();
  10.103 -(*9 secs*)
  10.104 -
  10.105 -writeln"Problem ~~5";
  10.106 -goal (theory "IFOLP") "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
  10.107 -by (IntPr.fast_tac 1);
  10.108 -result();
  10.109 -(*10 secs*)
  10.110 -
  10.111 -
  10.112 -writeln"Problem ~~6";
  10.113 -goal (theory "IFOLP") "?p : ~~(P | ~P)";
  10.114 -by (IntPr.fast_tac 1);
  10.115 -result();
  10.116 -
  10.117 -writeln"Problem ~~7";
  10.118 -goal (theory "IFOLP") "?p : ~~(P | ~~~P)";
  10.119 -by (IntPr.fast_tac 1);
  10.120 -result();
  10.121 -
  10.122 -writeln"Problem ~~8.  Peirce's law";
  10.123 -goal (theory "IFOLP") "?p : ~~(((P-->Q) --> P)  -->  P)";
  10.124 -by (IntPr.fast_tac 1);
  10.125 -result();
  10.126 -
  10.127 -writeln"Problem 9";
  10.128 -goal (theory "IFOLP") "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
  10.129 -by (IntPr.fast_tac 1);
  10.130 -result();
  10.131 -(*9 secs*)
  10.132 -
  10.133 -
  10.134 -writeln"Problem 10";
  10.135 -goal (theory "IFOLP") "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)";
  10.136 -by (IntPr.fast_tac 1);
  10.137 -result();
  10.138 -
  10.139 -writeln"11.  Proved in each direction (incorrectly, says Pelletier!!) ";
  10.140 -goal (theory "IFOLP") "?p : P<->P";
  10.141 -by (IntPr.fast_tac 1);
  10.142 -
  10.143 -writeln"Problem ~~12.  Dijkstra's law  ";
  10.144 -goal (theory "IFOLP") "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))";
  10.145 -by (IntPr.fast_tac 1);
  10.146 -result();
  10.147 -
  10.148 -goal (theory "IFOLP") "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))";
  10.149 -by (IntPr.fast_tac 1);
  10.150 -result();
  10.151 -
  10.152 -writeln"Problem 13.  Distributive law";
  10.153 -goal (theory "IFOLP") "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
  10.154 -by (IntPr.fast_tac 1);
  10.155 -result();
  10.156 -
  10.157 -writeln"Problem ~~14";
  10.158 -goal (theory "IFOLP") "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
  10.159 -by (IntPr.fast_tac 1);
  10.160 -result();
  10.161 -
  10.162 -writeln"Problem ~~15";
  10.163 -goal (theory "IFOLP") "?p : ~~((P --> Q) <-> (~P | Q))";
  10.164 -by (IntPr.fast_tac 1);
  10.165 -result();
  10.166 -
  10.167 -writeln"Problem ~~16";
  10.168 -goal (theory "IFOLP") "?p : ~~((P-->Q) | (Q-->P))";
  10.169 -by (IntPr.fast_tac 1);
  10.170 -result();
  10.171 -
  10.172 -writeln"Problem ~~17";
  10.173 -goal (theory "IFOLP")
  10.174 -  "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))";
  10.175 -by (IntPr.fast_tac 1);
  10.176 -(*over 5 minutes?? -- printing the proof term takes 40 secs!!*)
  10.177 -result();
  10.178 -
  10.179 -
  10.180 -writeln"** Examples with quantifiers **";
  10.181 -
  10.182 -writeln"The converse is classical in the following implications...";
  10.183 -
  10.184 -goal (theory "IFOLP") "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q";
  10.185 -by (IntPr.fast_tac 1); 
  10.186 -result();  
  10.187 -
  10.188 -goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
  10.189 -by (IntPr.fast_tac 1); 
  10.190 -result();  
  10.191 -
  10.192 -goal (theory "IFOLP") "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))";
  10.193 -by (IntPr.fast_tac 1); 
  10.194 -result();  
  10.195 -
  10.196 -goal (theory "IFOLP") "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)";
  10.197 -by (IntPr.fast_tac 1); 
  10.198 -result();  
  10.199 -
  10.200 -goal (theory "IFOLP") "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
  10.201 -by (IntPr.fast_tac 1);
  10.202 -result();  
  10.203 -
  10.204 -
  10.205 -
  10.206 -
  10.207 -writeln"The following are not constructively valid!";
  10.208 -(*The attempt to prove them terminates quickly!*)
  10.209 -
  10.210 -goal (theory "IFOLP") "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)";
  10.211 -by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
  10.212 -getgoal 1; 
  10.213 -
  10.214 -goal (theory "IFOLP") "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))";
  10.215 -by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
  10.216 -getgoal 1; 
  10.217 -
  10.218 -goal (theory "IFOLP") "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)";
  10.219 -by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
  10.220 -getgoal 1; 
  10.221 -
  10.222 -goal (theory "IFOLP") "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
  10.223 -by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
  10.224 -getgoal 1; 
  10.225 -
  10.226 -(*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
  10.227 -goal (theory "IFOLP") "?p : EX x. Q(x) --> (ALL x. Q(x))";
  10.228 -by (IntPr.fast_tac 1) handle ERROR _ => writeln"Failed, as expected";  
  10.229 -getgoal 1; 
  10.230 -
  10.231 -
  10.232 -writeln"Hard examples with quantifiers";
  10.233 -
  10.234 -(*The ones that have not been proved are not known to be valid!
  10.235 -  Some will require quantifier duplication -- not currently available*)
  10.236 -
  10.237 -writeln"Problem ~~18";
  10.238 -goal (theory "IFOLP") "?p : ~~(EX y. ALL x. P(y)-->P(x))";
  10.239 -(*NOT PROVED*)
  10.240 -
  10.241 -writeln"Problem ~~19";
  10.242 -goal (theory "IFOLP") "?p : ~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))";
  10.243 -(*NOT PROVED*)
  10.244 -
  10.245 -writeln"Problem 20";
  10.246 -goal (theory "IFOLP") "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
  10.247 -\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
  10.248 -by (IntPr.fast_tac 1); 
  10.249 -result();
  10.250 -
  10.251 -writeln"Problem 21";
  10.252 -goal (theory "IFOLP")
  10.253 -    "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))";
  10.254 -(*NOT PROVED*)
  10.255 -
  10.256 -writeln"Problem 22";
  10.257 -goal (theory "IFOLP") "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
  10.258 -by (IntPr.fast_tac 1); 
  10.259 -result();
  10.260 -
  10.261 -writeln"Problem ~~23";
  10.262 -goal (theory "IFOLP") "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))";
  10.263 -by (IntPr.best_tac 1);  
  10.264 -result();
  10.265 -
  10.266 -writeln"Problem 24";
  10.267 -goal (theory "IFOLP") "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
  10.268 -\    (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
  10.269 -\   --> ~~(EX x. P(x)&R(x))";
  10.270 -(*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
  10.271 -by IntPr.safe_tac; 
  10.272 -by (etac impE 1);
  10.273 -by (IntPr.fast_tac 1); 
  10.274 -by (IntPr.fast_tac 1); 
  10.275 -result();
  10.276 -
  10.277 -writeln"Problem 25";
  10.278 -goal (theory "IFOLP") "?p : (EX x. P(x)) &  \
  10.279 -\       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
  10.280 -\       (ALL x. P(x) --> (M(x) & L(x))) &   \
  10.281 -\       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
  10.282 -\   --> (EX x. Q(x)&P(x))";
  10.283 -by (IntPr.best_tac 1);
  10.284 -result();
  10.285 -
  10.286 -writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
  10.287 -goal (theory "IFOLP") "?p : (EX x. P(x)) & (EX y. Q(y))  \
  10.288 -\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
  10.289 -\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
  10.290 -by (IntPr.fast_tac 1); 
  10.291 -result();
  10.292 -
  10.293 -writeln"Problem ~~30";
  10.294 -goal (theory "IFOLP") "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & \
  10.295 -\       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
  10.296 -\   --> (ALL x. ~~S(x))";
  10.297 -by (IntPr.fast_tac 1);  
  10.298 -result();
  10.299 -
  10.300 -writeln"Problem 31";
  10.301 -goal (theory "IFOLP") "?p : ~(EX x. P(x) & (Q(x) | R(x))) & \
  10.302 -\       (EX x. L(x) & P(x)) & \
  10.303 -\       (ALL x. ~ R(x) --> M(x))  \
  10.304 -\   --> (EX x. L(x) & M(x))";
  10.305 -by (IntPr.fast_tac 1);
  10.306 -result();
  10.307 -
  10.308 -writeln"Problem 32";
  10.309 -goal (theory "IFOLP") "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
  10.310 -\       (ALL x. S(x) & R(x) --> L(x)) & \
  10.311 -\       (ALL x. M(x) --> R(x))  \
  10.312 -\   --> (ALL x. P(x) & M(x) --> L(x))";
  10.313 -by (IntPr.best_tac 1);  (*SLOW*)
  10.314 -result();
  10.315 -
  10.316 -writeln"Problem 39";
  10.317 -goal (theory "IFOLP") "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
  10.318 -by (IntPr.fast_tac 1);
  10.319 -result();
  10.320 -
  10.321 -writeln"Problem 40.  AMENDED";
  10.322 -goal (theory "IFOLP") "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
  10.323 -\             ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
  10.324 -by (IntPr.fast_tac 1);
  10.325 -result();
  10.326 -
  10.327 -writeln"Problem 44";
  10.328 -goal (theory "IFOLP") "?p : (ALL x. f(x) -->                                   \
  10.329 -\             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
  10.330 -\             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
  10.331 -\             --> (EX x. j(x) & ~f(x))";
  10.332 -by (IntPr.fast_tac 1);
  10.333 -result();
  10.334 -
  10.335 -writeln"Problem 48";
  10.336 -goal (theory "IFOLP") "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
  10.337 -by (IntPr.fast_tac 1);
  10.338 -result();
  10.339 -
  10.340 -writeln"Problem 51";
  10.341 -goal (theory "IFOLP")
  10.342 -    "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
  10.343 -\    (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
  10.344 -by (IntPr.best_tac 1);  (*60 seconds*)
  10.345 -result();
  10.346 -
  10.347 -writeln"Problem 56";
  10.348 -goal (theory "IFOLP")
  10.349 -    "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
  10.350 -by (IntPr.fast_tac 1);
  10.351 -result();
  10.352 -
  10.353 -writeln"Problem 57";
  10.354 -goal (theory "IFOLP")
  10.355 -    "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
  10.356 -\    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
  10.357 -by (IntPr.fast_tac 1);
  10.358 -result();
  10.359 -
  10.360 -writeln"Problem 60";
  10.361 -goal (theory "IFOLP")
  10.362 -    "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
  10.363 -by (IntPr.fast_tac 1);
  10.364 -result();
    11.1 --- a/src/FOLP/intprover.ML	Tue Mar 18 21:57:36 2008 +0100
    11.2 +++ b/src/FOLP/intprover.ML	Tue Mar 18 22:19:18 2008 +0100
    11.3 @@ -36,17 +36,17 @@
    11.4    step of an intuitionistic proof.
    11.5  *)
    11.6  val safe_brls = sort (make_ord lessb)
    11.7 -    [ (true,FalseE), (false,TrueI), (false,refl),
    11.8 -      (false,impI), (false,notI), (false,allI),
    11.9 -      (true,conjE), (true,exE),
   11.10 -      (false,conjI), (true,conj_impE),
   11.11 -      (true,disj_impE), (true,disjE), 
   11.12 -      (false,iffI), (true,iffE), (true,not_to_imp) ];
   11.13 +    [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}),
   11.14 +      (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
   11.15 +      (true, @{thm conjE}), (true, @{thm exE}),
   11.16 +      (false, @{thm conjI}), (true, @{thm conj_impE}),
   11.17 +      (true, @{thm disj_impE}), (true, @{thm disjE}), 
   11.18 +      (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ];
   11.19  
   11.20  val haz_brls =
   11.21 -    [ (false,disjI1), (false,disjI2), (false,exI), 
   11.22 -      (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
   11.23 -      (true,all_impE), (true,ex_impE), (true,impE) ];
   11.24 +    [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), 
   11.25 +      (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
   11.26 +      (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
   11.27  
   11.28  (*0 subgoals vs 1 or more: the p in safep is for positive*)
   11.29  val (safe0_brls, safep_brls) =
   11.30 @@ -76,4 +76,3 @@
   11.31    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
   11.32  
   11.33  end;
   11.34 -
    12.1 --- a/src/FOLP/simpdata.ML	Tue Mar 18 21:57:36 2008 +0100
    12.2 +++ b/src/FOLP/simpdata.ML	Tue Mar 18 22:19:18 2008 +0100
    12.3 @@ -6,86 +6,39 @@
    12.4  Simplification data for FOLP.
    12.5  *)
    12.6  
    12.7 -(*** Rewrite rules ***)
    12.8  
    12.9 -fun int_prove_fun_raw s =
   12.10 -    (writeln s;  prove_goal (the_context ()) s
   12.11 -       (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
   12.12 -
   12.13 -fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
   12.14 -
   12.15 -val conj_rews = map int_prove_fun
   12.16 - ["P & True <-> P",     "True & P <-> P",
   12.17 -  "P & False <-> False", "False & P <-> False",
   12.18 -  "P & P <-> P",
   12.19 -  "P & ~P <-> False",   "~P & P <-> False",
   12.20 -  "(P & Q) & R <-> P & (Q & R)"];
   12.21 -
   12.22 -val disj_rews = map int_prove_fun
   12.23 - ["P | True <-> True",  "True | P <-> True",
   12.24 -  "P | False <-> P",    "False | P <-> P",
   12.25 -  "P | P <-> P",
   12.26 -  "(P | Q) | R <-> P | (Q | R)"];
   12.27 -
   12.28 -val not_rews = map int_prove_fun
   12.29 - ["~ False <-> True",   "~ True <-> False"];
   12.30 +fun make_iff_T th = th RS @{thm P_Imp_P_iff_T};
   12.31  
   12.32 -val imp_rews = map int_prove_fun
   12.33 - ["(P --> False) <-> ~P",       "(P --> True) <-> True",
   12.34 -  "(False --> P) <-> True",     "(True --> P) <-> P",
   12.35 -  "(P --> P) <-> True",         "(P --> ~P) <-> ~P"];
   12.36 -
   12.37 -val iff_rews = map int_prove_fun
   12.38 - ["(True <-> P) <-> P",         "(P <-> True) <-> P",
   12.39 -  "(P <-> P) <-> True",
   12.40 -  "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
   12.41 -
   12.42 -val quant_rews = map int_prove_fun
   12.43 - ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
   12.44 +val refl_iff_T = make_iff_T @{thm refl};
   12.45  
   12.46 -(*These are NOT supplied by default!*)
   12.47 -val distrib_rews  = map int_prove_fun
   12.48 - ["~(P|Q) <-> ~P & ~Q",
   12.49 -  "P & (Q | R) <-> P&Q | P&R", "(Q | R) & P <-> Q&P | R&P",
   12.50 -  "(P | Q --> R) <-> (P --> R) & (Q --> R)",
   12.51 -  "~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))",
   12.52 -  "((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)",
   12.53 -  "(EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))",
   12.54 -  "NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"];
   12.55 -
   12.56 -val P_Imp_P_iff_T = int_prove_fun_raw "p:P ==> ?p:(P <-> True)";
   12.57 -
   12.58 -fun make_iff_T th = th RS P_Imp_P_iff_T;
   12.59 -
   12.60 -val refl_iff_T = make_iff_T refl;
   12.61 -
   12.62 -val norm_thms = [(norm_eq RS sym, norm_eq),
   12.63 -                 (NORM_iff RS iff_sym, NORM_iff)];
   12.64 +val norm_thms = [(@{thm norm_eq} RS @{thm sym}, @{thm norm_eq}),
   12.65 +                 (@{thm NORM_iff} RS @{thm iff_sym}, @{thm NORM_iff})];
   12.66  
   12.67  
   12.68  (* Conversion into rewrite rules *)
   12.69  
   12.70 -val not_P_imp_P_iff_F = int_prove_fun_raw "p:~P ==> ?p:(P <-> False)";
   12.71 -
   12.72  fun mk_eq th = case concl_of th of
   12.73 -      _ $ (Const("op <->",_)$_$_) $ _ => th
   12.74 -    | _ $ (Const("op =",_)$_$_) $ _ => th
   12.75 -    | _ $ (Const("Not",_)$_) $ _ => th RS not_P_imp_P_iff_F
   12.76 +      _ $ (Const (@{const_name "op <->"}, _) $ _ $ _) $ _ => th
   12.77 +    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) $ _ => th
   12.78 +    | _ $ (Const (@{const_name Not}, _) $ _) $ _ => th RS @{thm not_P_imp_P_iff_F}
   12.79      | _ => make_iff_T th;
   12.80  
   12.81  
   12.82  val mksimps_pairs =
   12.83 -  [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
   12.84 -   ("All", [spec]), ("True", []), ("False", [])];
   12.85 +  [(@{const_name "op -->"}, [@{thm mp}]),
   12.86 +   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
   12.87 +   (@{const_name "All"}, [@{thm spec}]),
   12.88 +   (@{const_name True}, []),
   12.89 +   (@{const_name False}, [])];
   12.90  
   12.91  fun mk_atomize pairs =
   12.92    let fun atoms th =
   12.93          (case concl_of th of
   12.94 -           Const("Trueprop",_) $ p =>
   12.95 +           Const ("Trueprop", _) $ p =>
   12.96               (case head_of p of
   12.97                  Const(a,_) =>
   12.98                    (case AList.lookup (op =) pairs a of
   12.99 -                     SOME(rls) => List.concat (map atoms ([th] RL rls))
  12.100 +                     SOME(rls) => maps atoms ([th] RL rls)
  12.101                     | NONE => [th])
  12.102                | _ => [th])
  12.103           | _ => [th])
  12.104 @@ -95,47 +48,40 @@
  12.105  
  12.106  (*destruct function for analysing equations*)
  12.107  fun dest_red(_ $ (red $ lhs $ rhs) $ _) = (red,lhs,rhs)
  12.108 -  | dest_red t = raise TERM("FOL/dest_red", [t]);
  12.109 +  | dest_red t = raise TERM("dest_red", [t]);
  12.110  
  12.111  structure FOLP_SimpData : SIMP_DATA =
  12.112 -  struct
  12.113 -  val refl_thms         = [refl, iff_refl]
  12.114 -  val trans_thms        = [trans, iff_trans]
  12.115 -  val red1              = iffD1
  12.116 -  val red2              = iffD2
  12.117 +struct
  12.118 +  val refl_thms         = [@{thm refl}, @{thm iff_refl}]
  12.119 +  val trans_thms        = [@{thm trans}, @{thm iff_trans}]
  12.120 +  val red1              = @{thm iffD1}
  12.121 +  val red2              = @{thm iffD2}
  12.122    val mk_rew_rules      = mk_rew_rules
  12.123    val case_splits       = []         (*NO IF'S!*)
  12.124    val norm_thms         = norm_thms
  12.125 -  val subst_thms        = [subst];
  12.126 +  val subst_thms        = [@{thm subst}];
  12.127    val dest_red          = dest_red
  12.128 -  end;
  12.129 +end;
  12.130  
  12.131  structure FOLP_Simp = SimpFun(FOLP_SimpData);
  12.132  
  12.133  (*not a component of SIMP_DATA, but an argument of SIMP_TAC *)
  12.134  val FOLP_congs =
  12.135 -   [all_cong,ex_cong,eq_cong,
  12.136 -    conj_cong,disj_cong,imp_cong,iff_cong,not_cong] @ pred_congs;
  12.137 +   [@{thm all_cong}, @{thm ex_cong}, @{thm eq_cong},
  12.138 +    @{thm conj_cong}, @{thm disj_cong}, @{thm imp_cong},
  12.139 +    @{thm iff_cong}, @{thm not_cong}] @ @{thms pred_congs};
  12.140  
  12.141  val IFOLP_rews =
  12.142 -   [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @
  12.143 -    imp_rews @ iff_rews @ quant_rews;
  12.144 +   [refl_iff_T] @ @{thms conj_rews} @ @{thms disj_rews} @ @{thms not_rews} @
  12.145 +    @{thms imp_rews} @ @{thms iff_rews} @ @{thms quant_rews};
  12.146  
  12.147  open FOLP_Simp;
  12.148  
  12.149 -val auto_ss = empty_ss setauto ares_tac [TrueI];
  12.150 +val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}];
  12.151  
  12.152  val IFOLP_ss = auto_ss addcongs FOLP_congs addrews IFOLP_rews;
  12.153  
  12.154 -(*Classical version...*)
  12.155 -fun prove_fun s =
  12.156 -    (writeln s;  prove_goal (the_context ()) s
  12.157 -       (fn prems => [ (cut_facts_tac prems 1), (Cla.fast_tac FOLP_cs 1) ]));
  12.158  
  12.159 -val cla_rews = map prove_fun
  12.160 - ["?p:P | ~P",          "?p:~P | P",
  12.161 -  "?p:~ ~ P <-> P",     "?p:(~P --> P) <-> P"];
  12.162 -
  12.163 -val FOLP_rews = IFOLP_rews@cla_rews;
  12.164 +val FOLP_rews = IFOLP_rews @ @{thms cla_rews};
  12.165  
  12.166  val FOLP_ss = auto_ss addcongs FOLP_congs addrews FOLP_rews;