proper bootstrap of IFOL/FOL theories and packages;
authorwenzelm
Wed Aug 25 20:45:19 1999 +0200 (1999-08-25 ago)
changeset 73554c43090659ca
parent 7354 358b1c5391f0
child 7356 1714c91b8729
proper bootstrap of IFOL/FOL theories and packages;
src/FOL/FOL.ML
src/FOL/FOL.thy
src/FOL/FOL_lemmas1.ML
src/FOL/FOL_lemmas2.ML
src/FOL/IFOL.ML
src/FOL/IFOL.thy
src/FOL/IFOL_lemmas.ML
src/FOL/IsaMakefile
src/FOL/ROOT.ML
src/FOL/blastdata.ML
src/FOL/cladata.ML
src/FOL/hypsubstdata.ML
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/FOL.ML	Wed Aug 25 20:42:01 1999 +0200
     1.2 +++ b/src/FOL/FOL.ML	Wed Aug 25 20:45:19 1999 +0200
     1.3 @@ -1,94 +1,8 @@
     1.4 -(*  Title:      FOL/FOL.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1991  University of Cambridge
     1.8  
     1.9 -Tactics and lemmas for FOL.thy (classical First-Order Logic)
    1.10 -*)
    1.11 +structure FOL =
    1.12 +struct
    1.13 +  val thy = the_context ();
    1.14 +  val classical = classical;
    1.15 +end;
    1.16  
    1.17  open FOL;
    1.18 -
    1.19 -
    1.20 -val ccontr = FalseE RS classical;
    1.21 -
    1.22 -(*** Classical introduction rules for | and EX ***)
    1.23 -
    1.24 -qed_goal "disjCI" FOL.thy 
    1.25 -   "(~Q ==> P) ==> P|Q"
    1.26 - (fn prems=>
    1.27 -  [ (rtac classical 1),
    1.28 -    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    1.29 -    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    1.30 -
    1.31 -(*introduction rule involving only EX*)
    1.32 -qed_goal "ex_classical" FOL.thy 
    1.33 -   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
    1.34 - (fn prems=>
    1.35 -  [ (rtac classical 1),
    1.36 -    (eresolve_tac (prems RL [exI]) 1) ]);
    1.37 -
    1.38 -(*version of above, simplifying ~EX to ALL~ *)
    1.39 -qed_goal "exCI" FOL.thy 
    1.40 -   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
    1.41 - (fn [prem]=>
    1.42 -  [ (rtac ex_classical 1),
    1.43 -    (resolve_tac [notI RS allI RS prem] 1),
    1.44 -    (etac notE 1),
    1.45 -    (etac exI 1) ]);
    1.46 -
    1.47 -qed_goal "excluded_middle" FOL.thy "~P | P"
    1.48 - (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    1.49 -
    1.50 -(*For disjunctive case analysis*)
    1.51 -fun excluded_middle_tac sP =
    1.52 -    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
    1.53 -
    1.54 -qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
    1.55 -  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
    1.56 -                  etac p2 1, etac p1 1]);
    1.57 -
    1.58 -(*HOL's more natural case analysis tactic*)
    1.59 -fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
    1.60 -
    1.61 -
    1.62 -(*** Special elimination rules *)
    1.63 -
    1.64 -
    1.65 -(*Classical implies (-->) elimination. *)
    1.66 -qed_goal "impCE" FOL.thy 
    1.67 -    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
    1.68 - (fn major::prems=>
    1.69 -  [ (resolve_tac [excluded_middle RS disjE] 1),
    1.70 -    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    1.71 -
    1.72 -(*This version of --> elimination works on Q before P.  It works best for
    1.73 -  those cases in which P holds "almost everywhere".  Can't install as
    1.74 -  default: would break old proofs.*)
    1.75 -qed_goal "impCE'" thy 
    1.76 -    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
    1.77 - (fn major::prems=>
    1.78 -  [ (resolve_tac [excluded_middle RS disjE] 1),
    1.79 -    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    1.80 -
    1.81 -(*Double negation law*)
    1.82 -qed_goal "notnotD" FOL.thy "~~P ==> P"
    1.83 - (fn [major]=>
    1.84 -  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
    1.85 -
    1.86 -qed_goal "contrapos2" FOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
    1.87 -        rtac classical 1,
    1.88 -        dtac p2 1,
    1.89 -        etac notE 1,
    1.90 -        rtac p1 1]);
    1.91 -
    1.92 -(*** Tactics for implication and contradiction ***)
    1.93 -
    1.94 -(*Classical <-> elimination.  Proof substitutes P=Q in 
    1.95 -    ~P ==> ~Q    and    P ==> Q  *)
    1.96 -qed_goalw "iffCE" FOL.thy [iff_def]
    1.97 -    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    1.98 - (fn prems =>
    1.99 -  [ (rtac conjE 1),
   1.100 -    (REPEAT (DEPTH_SOLVE_1 
   1.101 -        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
   1.102 -
     2.1 --- a/src/FOL/FOL.thy	Wed Aug 25 20:42:01 1999 +0200
     2.2 +++ b/src/FOL/FOL.thy	Wed Aug 25 20:45:19 1999 +0200
     2.3 @@ -1,10 +1,14 @@
     2.4  
     2.5 -FOL = IFOL +
     2.6 +theory FOL = IFOL
     2.7 +files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"):
     2.8  
     2.9 -rules
    2.10 -  classical "(~P ==> P) ==> P"
    2.11 +axioms
    2.12 +  classical: "(~P ==> P) ==> P"
    2.13  
    2.14 -setup ClasetThyData.setup
    2.15 -setup attrib_setup              (* FIXME move to IFOL.thy *)
    2.16 +use "FOL_lemmas1.ML"
    2.17 +use "cladata.ML"	setup Cla.setup setup clasetup
    2.18 +use "blastdata.ML"	setup Blast.setup
    2.19 +use "FOL_lemmas2.ML"
    2.20 +use "simpdata.ML"	setup simpsetup setup Clasimp.setup
    2.21  
    2.22  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/FOL/FOL_lemmas1.ML	Wed Aug 25 20:45:19 1999 +0200
     3.3 @@ -0,0 +1,92 @@
     3.4 +(*  Title:      FOL/FOL_lemmas1.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1991  University of Cambridge
     3.8 +
     3.9 +Tactics and lemmas for theory FOL (classical First-Order Logic).
    3.10 +*)
    3.11 +
    3.12 +val classical = thm "classical";
    3.13 +val ccontr = FalseE RS classical;
    3.14 +
    3.15 +
    3.16 +(*** Classical introduction rules for | and EX ***)
    3.17 +
    3.18 +qed_goal "disjCI" (the_context ()) 
    3.19 +   "(~Q ==> P) ==> P|Q"
    3.20 + (fn prems=>
    3.21 +  [ (rtac classical 1),
    3.22 +    (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
    3.23 +    (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
    3.24 +
    3.25 +(*introduction rule involving only EX*)
    3.26 +qed_goal "ex_classical" (the_context ()) 
    3.27 +   "( ~(EX x. P(x)) ==> P(a)) ==> EX x. P(x)"
    3.28 + (fn prems=>
    3.29 +  [ (rtac classical 1),
    3.30 +    (eresolve_tac (prems RL [exI]) 1) ]);
    3.31 +
    3.32 +(*version of above, simplifying ~EX to ALL~ *)
    3.33 +qed_goal "exCI" (the_context ()) 
    3.34 +   "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)"
    3.35 + (fn [prem]=>
    3.36 +  [ (rtac ex_classical 1),
    3.37 +    (resolve_tac [notI RS allI RS prem] 1),
    3.38 +    (etac notE 1),
    3.39 +    (etac exI 1) ]);
    3.40 +
    3.41 +qed_goal "excluded_middle" (the_context ()) "~P | P"
    3.42 + (fn _=> [ rtac disjCI 1, assume_tac 1 ]);
    3.43 +
    3.44 +(*For disjunctive case analysis*)
    3.45 +fun excluded_middle_tac sP =
    3.46 +    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
    3.47 +
    3.48 +qed_goal "case_split_thm" (the_context ()) "[| P ==> Q; ~P ==> Q |] ==> Q"
    3.49 +  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
    3.50 +                  etac p2 1, etac p1 1]);
    3.51 +
    3.52 +(*HOL's more natural case analysis tactic*)
    3.53 +fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
    3.54 +
    3.55 +
    3.56 +(*** Special elimination rules *)
    3.57 +
    3.58 +
    3.59 +(*Classical implies (-->) elimination. *)
    3.60 +qed_goal "impCE" (the_context ()) 
    3.61 +    "[| P-->Q;  ~P ==> R;  Q ==> R |] ==> R"
    3.62 + (fn major::prems=>
    3.63 +  [ (resolve_tac [excluded_middle RS disjE] 1),
    3.64 +    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    3.65 +
    3.66 +(*This version of --> elimination works on Q before P.  It works best for
    3.67 +  those cases in which P holds "almost everywhere".  Can't install as
    3.68 +  default: would break old proofs.*)
    3.69 +qed_goal "impCE'" (the_context ()) 
    3.70 +    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
    3.71 + (fn major::prems=>
    3.72 +  [ (resolve_tac [excluded_middle RS disjE] 1),
    3.73 +    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    3.74 +
    3.75 +(*Double negation law*)
    3.76 +qed_goal "notnotD" (the_context ()) "~~P ==> P"
    3.77 + (fn [major]=>
    3.78 +  [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
    3.79 +
    3.80 +qed_goal "contrapos2" (the_context ()) "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
    3.81 +        rtac classical 1,
    3.82 +        dtac p2 1,
    3.83 +        etac notE 1,
    3.84 +        rtac p1 1]);
    3.85 +
    3.86 +(*** Tactics for implication and contradiction ***)
    3.87 +
    3.88 +(*Classical <-> elimination.  Proof substitutes P=Q in 
    3.89 +    ~P ==> ~Q    and    P ==> Q  *)
    3.90 +qed_goalw "iffCE" (the_context ()) [iff_def]
    3.91 +    "[| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
    3.92 + (fn prems =>
    3.93 +  [ (rtac conjE 1),
    3.94 +    (REPEAT (DEPTH_SOLVE_1 
    3.95 +        (etac impCE 1  ORELSE  mp_tac 1  ORELSE  ares_tac prems 1))) ]);
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/FOL/FOL_lemmas2.ML	Wed Aug 25 20:45:19 1999 +0200
     4.3 @@ -0,0 +1,4 @@
     4.4 +
     4.5 +Goal "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c";
     4.6 +  by (Blast_tac 1);
     4.7 +qed "ex1_functional";
     5.1 --- a/src/FOL/IFOL.ML	Wed Aug 25 20:42:01 1999 +0200
     5.2 +++ b/src/FOL/IFOL.ML	Wed Aug 25 20:45:19 1999 +0200
     5.3 @@ -1,454 +1,28 @@
     5.4 -(*  Title:      FOL/IFOL.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1992  University of Cambridge
     5.8  
     5.9 -Tactics and lemmas for IFOL.thy (intuitionistic first-order logic)
    5.10 -*)
    5.11 -
    5.12 -qed_goalw "TrueI" IFOL.thy [True_def] "True"
    5.13 - (fn _ => [ (REPEAT (ares_tac [impI] 1)) ]);
    5.14 -
    5.15 -(*** Sequent-style elimination rules for & --> and ALL ***)
    5.16 -
    5.17 -qed_goal "conjE" IFOL.thy 
    5.18 -    "[| P&Q; [| P; Q |] ==> R |] ==> R"
    5.19 - (fn prems=>
    5.20 -  [ (REPEAT (resolve_tac prems 1
    5.21 -      ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN
    5.22 -              resolve_tac prems 1))) ]);
    5.23 -
    5.24 -qed_goal "impE" IFOL.thy 
    5.25 -    "[| P-->Q;  P;  Q ==> R |] ==> R"
    5.26 - (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    5.27 -
    5.28 -qed_goal "allE" IFOL.thy 
    5.29 -    "[| ALL x. P(x); P(x) ==> R |] ==> R"
    5.30 - (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    5.31 -
    5.32 -(*Duplicates the quantifier; for use with eresolve_tac*)
    5.33 -qed_goal "all_dupE" IFOL.thy 
    5.34 -    "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R \
    5.35 -\    |] ==> R"
    5.36 - (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    5.37 -
    5.38 -
    5.39 -(*** Negation rules, which translate between ~P and P-->False ***)
    5.40 -
    5.41 -qed_goalw "notI" IFOL.thy [not_def] "(P ==> False) ==> ~P"
    5.42 - (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
    5.43 -
    5.44 -qed_goalw "notE" IFOL.thy [not_def] "[| ~P;  P |] ==> R"
    5.45 - (fn prems=>
    5.46 -  [ (resolve_tac [mp RS FalseE] 1),
    5.47 -    (REPEAT (resolve_tac prems 1)) ]);
    5.48 -
    5.49 -qed_goal "rev_notE" IFOL.thy "!!P R. [| P; ~P |] ==> R"
    5.50 - (fn _ => [REPEAT (ares_tac [notE] 1)]);
    5.51 -
    5.52 -(*This is useful with the special implication rules for each kind of P. *)
    5.53 -qed_goal "not_to_imp" IFOL.thy 
    5.54 -    "[| ~P;  (P-->False) ==> Q |] ==> Q"
    5.55 - (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
    5.56 -
    5.57 -(* For substitution into an assumption P, reduce Q to P-->Q, substitute into
    5.58 -   this implication, then apply impI to move P back into the assumptions.
    5.59 -   To specify P use something like
    5.60 -      eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
    5.61 -qed_goal "rev_mp" IFOL.thy "[| P;  P --> Q |] ==> Q"
    5.62 - (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    5.63 -
    5.64 -(*Contrapositive of an inference rule*)
    5.65 -qed_goal "contrapos" IFOL.thy "[| ~Q;  P==>Q |] ==> ~P"
    5.66 - (fn [major,minor]=> 
    5.67 -  [ (rtac (major RS notE RS notI) 1), 
    5.68 -    (etac minor 1) ]);
    5.69 -
    5.70 -
    5.71 -(*** Modus Ponens Tactics ***)
    5.72 -
    5.73 -(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    5.74 -fun mp_tac i = eresolve_tac [notE,impE] i  THEN  assume_tac i;
    5.75 -
    5.76 -(*Like mp_tac but instantiates no variables*)
    5.77 -fun eq_mp_tac i = eresolve_tac [notE,impE] i  THEN  eq_assume_tac i;
    5.78 -
    5.79 -
    5.80 -(*** If-and-only-if ***)
    5.81 -
    5.82 -qed_goalw "iffI" IFOL.thy [iff_def]
    5.83 -   "[| P ==> Q;  Q ==> P |] ==> P<->Q"
    5.84 - (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
    5.85 -
    5.86 -
    5.87 -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
    5.88 -qed_goalw "iffE" IFOL.thy [iff_def]
    5.89 -    "[| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R"
    5.90 - (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);
    5.91 -
    5.92 -(* Destruct rules for <-> similar to Modus Ponens *)
    5.93 -
    5.94 -qed_goalw "iffD1" IFOL.thy [iff_def] "[| P <-> Q;  P |] ==> Q"
    5.95 - (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
    5.96 -
    5.97 -qed_goalw "iffD2" IFOL.thy [iff_def] "[| P <-> Q;  Q |] ==> P"
    5.98 - (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
    5.99 -
   5.100 -qed_goal "rev_iffD1" IFOL.thy "!!P. [| P; P <-> Q |] ==> Q"
   5.101 - (fn _ => [etac iffD1 1, assume_tac 1]);
   5.102 -
   5.103 -qed_goal "rev_iffD2" IFOL.thy "!!P. [| Q; P <-> Q |] ==> P"
   5.104 - (fn _ => [etac iffD2 1, assume_tac 1]);
   5.105 -
   5.106 -qed_goal "iff_refl" IFOL.thy "P <-> P"
   5.107 - (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]);
   5.108 -
   5.109 -qed_goal "iff_sym" IFOL.thy "Q <-> P ==> P <-> Q"
   5.110 - (fn [major] =>
   5.111 -  [ (rtac (major RS iffE) 1),
   5.112 -    (rtac iffI 1),
   5.113 -    (REPEAT (eresolve_tac [asm_rl,mp] 1)) ]);
   5.114 -
   5.115 -qed_goal "iff_trans" IFOL.thy
   5.116 -    "!!P Q R. [| P <-> Q;  Q<-> R |] ==> P <-> R"
   5.117 - (fn _ =>
   5.118 -  [ (rtac iffI 1),
   5.119 -    (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]);
   5.120 -
   5.121 -
   5.122 -(*** Unique existence.  NOTE THAT the following 2 quantifications
   5.123 -   EX!x such that [EX!y such that P(x,y)]     (sequential)
   5.124 -   EX!x,y such that P(x,y)                    (simultaneous)
   5.125 - do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   5.126 -***)
   5.127 -
   5.128 -qed_goalw "ex1I" IFOL.thy [ex1_def]
   5.129 -    "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)"
   5.130 - (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
   5.131 -
   5.132 -(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   5.133 -qed_goal "ex_ex1I" IFOL.thy
   5.134 -    "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
   5.135 - (fn [ex,eq] => [ (rtac (ex RS exE) 1),
   5.136 -                  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
   5.137 -
   5.138 -qed_goalw "ex1E" IFOL.thy [ex1_def]
   5.139 -    "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
   5.140 - (fn prems =>
   5.141 -  [ (cut_facts_tac prems 1),
   5.142 -    (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]);
   5.143 -
   5.144 -
   5.145 -(*** <-> congruence rules for simplification ***)
   5.146 -
   5.147 -(*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
   5.148 -fun iff_tac prems i =
   5.149 -    resolve_tac (prems RL [iffE]) i THEN
   5.150 -    REPEAT1 (eresolve_tac [asm_rl,mp] i);
   5.151 -
   5.152 -qed_goal "conj_cong" IFOL.thy 
   5.153 -    "[| P <-> P';  P' ==> Q <-> Q' |] ==> (P&Q) <-> (P'&Q')"
   5.154 - (fn prems =>
   5.155 -  [ (cut_facts_tac prems 1),
   5.156 -    (REPEAT  (ares_tac [iffI,conjI] 1
   5.157 -      ORELSE  eresolve_tac [iffE,conjE,mp] 1
   5.158 -      ORELSE  iff_tac prems 1)) ]);
   5.159 -
   5.160 -(*Reversed congruence rule!   Used in ZF/Order*)
   5.161 -qed_goal "conj_cong2" IFOL.thy 
   5.162 -    "[| P <-> P';  P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')"
   5.163 - (fn prems =>
   5.164 -  [ (cut_facts_tac prems 1),
   5.165 -    (REPEAT  (ares_tac [iffI,conjI] 1
   5.166 -      ORELSE  eresolve_tac [iffE,conjE,mp] 1
   5.167 -      ORELSE  iff_tac prems 1)) ]);
   5.168 -
   5.169 -qed_goal "disj_cong" IFOL.thy 
   5.170 -    "[| P <-> P';  Q <-> Q' |] ==> (P|Q) <-> (P'|Q')"
   5.171 - (fn prems =>
   5.172 -  [ (cut_facts_tac prems 1),
   5.173 -    (REPEAT  (eresolve_tac [iffE,disjE,disjI1,disjI2] 1
   5.174 -      ORELSE  ares_tac [iffI] 1
   5.175 -      ORELSE  mp_tac 1)) ]);
   5.176 -
   5.177 -qed_goal "imp_cong" IFOL.thy 
   5.178 -    "[| P <-> P';  P' ==> Q <-> Q' |] ==> (P-->Q) <-> (P'-->Q')"
   5.179 - (fn prems =>
   5.180 -  [ (cut_facts_tac prems 1),
   5.181 -    (REPEAT   (ares_tac [iffI,impI] 1
   5.182 -      ORELSE  etac iffE 1
   5.183 -      ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
   5.184 -
   5.185 -qed_goal "iff_cong" IFOL.thy 
   5.186 -    "[| P <-> P';  Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
   5.187 - (fn prems =>
   5.188 -  [ (cut_facts_tac prems 1),
   5.189 -    (REPEAT   (etac iffE 1
   5.190 -      ORELSE  ares_tac [iffI] 1
   5.191 -      ORELSE  mp_tac 1)) ]);
   5.192 -
   5.193 -qed_goal "not_cong" IFOL.thy 
   5.194 -    "P <-> P' ==> ~P <-> ~P'"
   5.195 - (fn prems =>
   5.196 -  [ (cut_facts_tac prems 1),
   5.197 -    (REPEAT   (ares_tac [iffI,notI] 1
   5.198 -      ORELSE  mp_tac 1
   5.199 -      ORELSE  eresolve_tac [iffE,notE] 1)) ]);
   5.200 -
   5.201 -qed_goal "all_cong" IFOL.thy 
   5.202 -    "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
   5.203 - (fn prems =>
   5.204 -  [ (REPEAT   (ares_tac [iffI,allI] 1
   5.205 -      ORELSE   mp_tac 1
   5.206 -      ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
   5.207 -
   5.208 -qed_goal "ex_cong" IFOL.thy 
   5.209 -    "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
   5.210 - (fn prems =>
   5.211 -  [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   5.212 -      ORELSE   mp_tac 1
   5.213 -      ORELSE   iff_tac prems 1)) ]);
   5.214 -
   5.215 -qed_goal "ex1_cong" IFOL.thy 
   5.216 -    "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))"
   5.217 - (fn prems =>
   5.218 -  [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
   5.219 -      ORELSE   mp_tac 1
   5.220 -      ORELSE   iff_tac prems 1)) ]);
   5.221 -
   5.222 -(*** Equality rules ***)
   5.223 -
   5.224 -qed_goal "sym" IFOL.thy "a=b ==> b=a"
   5.225 - (fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]);
   5.226 -
   5.227 -qed_goal "trans" IFOL.thy "[| a=b;  b=c |] ==> a=c"
   5.228 - (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]);
   5.229 -
   5.230 -(** ~ b=a ==> ~ a=b **)
   5.231 -val [not_sym] = compose(sym,2,contrapos);
   5.232 -
   5.233 -
   5.234 -(* Two theorms for rewriting only one instance of a definition:
   5.235 -   the first for definitions of formulae and the second for terms *)
   5.236 -
   5.237 -val prems = goal IFOL.thy "(A == B) ==> A <-> B";
   5.238 -by (rewrite_goals_tac prems);
   5.239 -by (rtac iff_refl 1);
   5.240 -qed "def_imp_iff";
   5.241 -
   5.242 -val prems = goal IFOL.thy "(A == B) ==> A = B";
   5.243 -by (rewrite_goals_tac prems);
   5.244 -by (rtac refl 1);
   5.245 -qed "meta_eq_to_obj_eq";
   5.246 -
   5.247 -
   5.248 -(*Substitution: rule and tactic*)
   5.249 -bind_thm ("ssubst", sym RS subst);
   5.250 -
   5.251 -(*Apply an equality or definition ONCE.
   5.252 -  Fails unless the substitution has an effect*)
   5.253 -fun stac th = 
   5.254 -  let val th' = th RS meta_eq_to_obj_eq handle THM _ => th
   5.255 -  in  CHANGED_GOAL (rtac (th' RS ssubst))
   5.256 -  end;
   5.257 -
   5.258 -(*A special case of ex1E that would otherwise need quantifier expansion*)
   5.259 -qed_goal "ex1_equalsE" IFOL.thy
   5.260 -    "[| EX! x. P(x);  P(a);  P(b) |] ==> a=b"
   5.261 - (fn prems =>
   5.262 -  [ (cut_facts_tac prems 1),
   5.263 -    (etac ex1E 1),
   5.264 -    (rtac trans 1),
   5.265 -    (rtac sym 2),
   5.266 -    (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]);
   5.267 -
   5.268 -(** Polymorphic congruence rules **)
   5.269 -
   5.270 -qed_goal "subst_context" IFOL.thy 
   5.271 -   "[| a=b |]  ==>  t(a)=t(b)"
   5.272 - (fn prems=>
   5.273 -  [ (resolve_tac (prems RL [ssubst]) 1),
   5.274 -    (rtac refl 1) ]);
   5.275 -
   5.276 -qed_goal "subst_context2" IFOL.thy 
   5.277 -   "[| a=b;  c=d |]  ==>  t(a,c)=t(b,d)"
   5.278 - (fn prems=>
   5.279 -  [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   5.280 -
   5.281 -qed_goal "subst_context3" IFOL.thy 
   5.282 -   "[| a=b;  c=d;  e=f |]  ==>  t(a,c,e)=t(b,d,f)"
   5.283 - (fn prems=>
   5.284 -  [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   5.285 -
   5.286 -(*Useful with eresolve_tac for proving equalties from known equalities.
   5.287 -        a = b
   5.288 -        |   |
   5.289 -        c = d   *)
   5.290 -qed_goal "box_equals" IFOL.thy
   5.291 -    "[| a=b;  a=c;  b=d |] ==> c=d"  
   5.292 - (fn prems=>
   5.293 -  [ (rtac trans 1),
   5.294 -    (rtac trans 1),
   5.295 -    (rtac sym 1),
   5.296 -    (REPEAT (resolve_tac prems 1)) ]);
   5.297 -
   5.298 -(*Dual of box_equals: for proving equalities backwards*)
   5.299 -qed_goal "simp_equals" IFOL.thy
   5.300 -    "[| a=c;  b=d;  c=d |] ==> a=b"  
   5.301 - (fn prems=>
   5.302 -  [ (rtac trans 1),
   5.303 -    (rtac trans 1),
   5.304 -    (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]);
   5.305 -
   5.306 -(** Congruence rules for predicate letters **)
   5.307 -
   5.308 -qed_goal "pred1_cong" IFOL.thy
   5.309 -    "a=a' ==> P(a) <-> P(a')"
   5.310 - (fn prems =>
   5.311 -  [ (cut_facts_tac prems 1),
   5.312 -    (rtac iffI 1),
   5.313 -    (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   5.314 -
   5.315 -qed_goal "pred2_cong" IFOL.thy
   5.316 -    "[| a=a';  b=b' |] ==> P(a,b) <-> P(a',b')"
   5.317 - (fn prems =>
   5.318 -  [ (cut_facts_tac prems 1),
   5.319 -    (rtac iffI 1),
   5.320 -    (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   5.321 -
   5.322 -qed_goal "pred3_cong" IFOL.thy
   5.323 -    "[| a=a';  b=b';  c=c' |] ==> P(a,b,c) <-> P(a',b',c')"
   5.324 - (fn prems =>
   5.325 -  [ (cut_facts_tac prems 1),
   5.326 -    (rtac iffI 1),
   5.327 -    (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   5.328 -
   5.329 -(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   5.330 -
   5.331 -val pred_congs = 
   5.332 -    flat (map (fn c => 
   5.333 -               map (fn th => read_instantiate [("P",c)] th)
   5.334 -                   [pred1_cong,pred2_cong,pred3_cong])
   5.335 -               (explode"PQRS"));
   5.336 -
   5.337 -(*special case for the equality predicate!*)
   5.338 -val eq_cong = read_instantiate [("P","op =")] pred2_cong;
   5.339 -
   5.340 -
   5.341 -(*** Simplifications of assumed implications.
   5.342 -     Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
   5.343 -     used with mp_tac (restricted to atomic formulae) is COMPLETE for 
   5.344 -     intuitionistic propositional logic.  See
   5.345 -   R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   5.346 -    (preprint, University of St Andrews, 1991)  ***)
   5.347 -
   5.348 -qed_goal "conj_impE" IFOL.thy 
   5.349 -    "[| (P&Q)-->S;  P-->(Q-->S) ==> R |] ==> R"
   5.350 - (fn major::prems=>
   5.351 -  [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
   5.352 -
   5.353 -qed_goal "disj_impE" IFOL.thy 
   5.354 -    "[| (P|Q)-->S;  [| P-->S; Q-->S |] ==> R |] ==> R"
   5.355 - (fn major::prems=>
   5.356 -  [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]);
   5.357 -
   5.358 -(*Simplifies the implication.  Classical version is stronger. 
   5.359 -  Still UNSAFE since Q must be provable -- backtracking needed.  *)
   5.360 -qed_goal "imp_impE" IFOL.thy 
   5.361 -    "[| (P-->Q)-->S;  [| P; Q-->S |] ==> Q;  S ==> R |] ==> R"
   5.362 - (fn major::prems=>
   5.363 -  [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
   5.364 -
   5.365 -(*Simplifies the implication.  Classical version is stronger. 
   5.366 -  Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   5.367 -qed_goal "not_impE" IFOL.thy
   5.368 -    "[| ~P --> S;  P ==> False;  S ==> R |] ==> R"
   5.369 - (fn major::prems=>
   5.370 -  [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
   5.371 -
   5.372 -(*Simplifies the implication.   UNSAFE.  *)
   5.373 -qed_goal "iff_impE" IFOL.thy 
   5.374 -    "[| (P<->Q)-->S;  [| P; Q-->S |] ==> Q;  [| Q; P-->S |] ==> P;  \
   5.375 -\       S ==> R |] ==> R"
   5.376 - (fn major::prems=>
   5.377 -  [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
   5.378 -
   5.379 -(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   5.380 -qed_goal "all_impE" IFOL.thy 
   5.381 -    "[| (ALL x. P(x))-->S;  !!x. P(x);  S ==> R |] ==> R"
   5.382 - (fn major::prems=>
   5.383 -  [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
   5.384 -
   5.385 -(*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   5.386 -qed_goal "ex_impE" IFOL.thy 
   5.387 -    "[| (EX x. P(x))-->S;  P(x)-->S ==> R |] ==> R"
   5.388 - (fn major::prems=>
   5.389 -  [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
   5.390 -
   5.391 -(*** Courtesy of Krzysztof Grabczewski ***)
   5.392 -
   5.393 -val major::prems = goal IFOL.thy "[| P|Q;  P==>R;  Q==>S |] ==> R|S";
   5.394 -by (rtac (major RS disjE) 1);
   5.395 -by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
   5.396 -qed "disj_imp_disj";
   5.397 -
   5.398 -
   5.399 -(** strip ALL and --> from proved goal while preserving ALL-bound var names **)
   5.400 -
   5.401 -fun make_new_spec rl =
   5.402 -  (* Use a crazy name to avoid forall_intr failing because of
   5.403 -     duplicate variable name *)
   5.404 -  let val myspec = read_instantiate [("P","?wlzickd")] rl
   5.405 -      val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
   5.406 -      val cvx = cterm_of (#sign(rep_thm myspec)) vx
   5.407 -  in (vxT, forall_intr cvx myspec) end;
   5.408 -
   5.409 -local
   5.410 -
   5.411 -val (specT,  spec')  = make_new_spec spec
   5.412 -
   5.413 -in
   5.414 -
   5.415 -fun RSspec th =
   5.416 -  (case concl_of th of
   5.417 -     _ $ (Const("All",_) $ Abs(a,_,_)) =>
   5.418 -         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT))
   5.419 -         in th RS forall_elim ca spec' end
   5.420 -  | _ => raise THM("RSspec",0,[th]));
   5.421 -
   5.422 -fun RSmp th =
   5.423 -  (case concl_of th of
   5.424 -     _ $ (Const("op -->",_)$_$_) => th RS mp
   5.425 -  | _ => raise THM("RSmp",0,[th]));
   5.426 -
   5.427 -fun normalize_thm funs =
   5.428 -  let fun trans [] th = th
   5.429 -	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   5.430 -  in trans funs end;
   5.431 -
   5.432 -fun qed_spec_mp name =
   5.433 -  let val thm = normalize_thm [RSspec,RSmp] (result())
   5.434 -  in bind_thm(name, thm) end;
   5.435 -
   5.436 -fun qed_goal_spec_mp name thy s p = 
   5.437 -      bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   5.438 -
   5.439 -fun qed_goalw_spec_mp name thy defs s p = 
   5.440 -      bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   5.441 -
   5.442 +structure IFOL =
   5.443 +struct
   5.444 +  val thy = the_context ();
   5.445 +  val refl = refl;
   5.446 +  val subst = subst;
   5.447 +  val conjI = conjI;
   5.448 +  val conjunct1 = conjunct1;
   5.449 +  val conjunct2 = conjunct2;
   5.450 +  val disjI1 = disjI1;
   5.451 +  val disjI2 = disjI2;
   5.452 +  val disjE = disjE;
   5.453 +  val impI = impI;
   5.454 +  val mp = mp;
   5.455 +  val FalseE = FalseE;
   5.456 +  val True_def = True_def;
   5.457 +  val not_def = not_def;
   5.458 +  val iff_def = iff_def;
   5.459 +  val ex1_def = ex1_def;
   5.460 +  val allI = allI;
   5.461 +  val spec = spec;
   5.462 +  val exI = exI;
   5.463 +  val exE = exE;
   5.464 +  val eq_reflection = eq_reflection;
   5.465 +  val iff_reflection = iff_reflection;
   5.466  end;
   5.467  
   5.468 -
   5.469 -(* attributes *)
   5.470 -
   5.471 -local
   5.472 -
   5.473 -fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
   5.474 -
   5.475 -in
   5.476 -
   5.477 -val attrib_setup =
   5.478 - [Attrib.add_attributes
   5.479 -  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
   5.480 -
   5.481 -end;
   5.482 +open IFOL;
     6.1 --- a/src/FOL/IFOL.thy	Wed Aug 25 20:42:01 1999 +0200
     6.2 +++ b/src/FOL/IFOL.thy	Wed Aug 25 20:45:19 1999 +0200
     6.3 @@ -6,120 +6,121 @@
     6.4  Intuitionistic first-order logic.
     6.5  *)
     6.6  
     6.7 -IFOL = Pure +
     6.8 +theory IFOL = Pure
     6.9 +files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"):
    6.10 +
    6.11  
    6.12  global
    6.13  
    6.14 -classes
    6.15 -  term < logic
    6.16 -
    6.17 -default
    6.18 -  term
    6.19 +classes "term" < logic
    6.20 +defaultsort "term"
    6.21  
    6.22 -types
    6.23 -  o
    6.24 -
    6.25 -arities
    6.26 -  o :: logic
    6.27 -
    6.28 +typedecl o
    6.29  
    6.30  consts
    6.31  
    6.32 -  Trueprop      :: o => prop                    ("(_)" 5)
    6.33 -  True, False   :: o
    6.34 +  Trueprop      :: "o => prop"                  ("(_)" 5)
    6.35 +  True          :: o
    6.36 +  False         :: o
    6.37  
    6.38    (* Connectives *)
    6.39  
    6.40 -  "="           :: ['a, 'a] => o                (infixl 50)
    6.41 +  "="           :: "['a, 'a] => o"              (infixl 50)
    6.42  
    6.43 -  Not           :: o => o                       ("~ _" [40] 40)
    6.44 -  "&"           :: [o, o] => o                  (infixr 35)
    6.45 -  "|"           :: [o, o] => o                  (infixr 30)
    6.46 -  "-->"         :: [o, o] => o                  (infixr 25)
    6.47 -  "<->"         :: [o, o] => o                  (infixr 25)
    6.48 +  Not           :: "o => o"                     ("~ _" [40] 40)
    6.49 +  &             :: "[o, o] => o"                (infixr 35)
    6.50 +  "|"           :: "[o, o] => o"                (infixr 30)
    6.51 +  -->           :: "[o, o] => o"                (infixr 25)
    6.52 +  <->           :: "[o, o] => o"                (infixr 25)
    6.53  
    6.54    (* Quantifiers *)
    6.55  
    6.56 -  All           :: ('a => o) => o               (binder "ALL " 10)
    6.57 -  Ex            :: ('a => o) => o               (binder "EX " 10)
    6.58 -  Ex1           :: ('a => o) => o               (binder "EX! " 10)
    6.59 +  All           :: "('a => o) => o"             (binder "ALL " 10)
    6.60 +  Ex            :: "('a => o) => o"             (binder "EX " 10)
    6.61 +  Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    6.62  
    6.63  
    6.64  
    6.65  syntax
    6.66 -  "~="          :: ['a, 'a] => o                (infixl 50)
    6.67 +  "~="          :: "['a, 'a] => o"              (infixl 50)
    6.68  
    6.69  translations
    6.70    "x ~= y"      == "~ (x = y)"
    6.71  
    6.72  syntax (symbols)
    6.73 -  Not           :: o => o                       ("\\<not> _" [40] 40)
    6.74 -  "op &"        :: [o, o] => o                  (infixr "\\<and>" 35)
    6.75 -  "op |"        :: [o, o] => o                  (infixr "\\<or>" 30)
    6.76 -  "op -->"      :: [o, o] => o                  (infixr "\\<midarrow>\\<rightarrow>" 25)
    6.77 -  "op <->"      :: [o, o] => o                  (infixr "\\<leftarrow>\\<rightarrow>" 25)
    6.78 -  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" [0, 10] 10)
    6.79 -  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" [0, 10] 10)
    6.80 -  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
    6.81 -  "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
    6.82 +  Not           :: "o => o"                     ("\\<not> _" [40] 40)
    6.83 +  "op &"        :: "[o, o] => o"                (infixr "\\<and>" 35)
    6.84 +  "op |"        :: "[o, o] => o"                (infixr "\\<or>" 30)
    6.85 +  "op -->"      :: "[o, o] => o"                (infixr "\\<midarrow>\\<rightarrow>" 25)
    6.86 +  "op <->"      :: "[o, o] => o"                (infixr "\\<leftarrow>\\<rightarrow>" 25)
    6.87 +  "ALL "        :: "[idts, o] => o"             ("(3\\<forall>_./ _)" [0, 10] 10)
    6.88 +  "EX "         :: "[idts, o] => o"             ("(3\\<exists>_./ _)" [0, 10] 10)
    6.89 +  "EX! "        :: "[idts, o] => o"             ("(3\\<exists>!_./ _)" [0, 10] 10)
    6.90 +  "op ~="       :: "['a, 'a] => o"              (infixl "\\<noteq>" 50)
    6.91  
    6.92  syntax (xsymbols)
    6.93 -  "op -->"      :: [o, o] => o                  (infixr "\\<longrightarrow>" 25)
    6.94 -  "op <->"      :: [o, o] => o                  (infixr "\\<longleftrightarrow>" 25)
    6.95 +  "op -->"      :: "[o, o] => o"                (infixr "\\<longrightarrow>" 25)
    6.96 +  "op <->"      :: "[o, o] => o"                (infixr "\\<longleftrightarrow>" 25)
    6.97  
    6.98  syntax (HTML output)
    6.99 -  Not           :: o => o                       ("\\<not> _" [40] 40)
   6.100 +  Not           :: "o => o"                     ("\\<not> _" [40] 40)
   6.101  
   6.102  
   6.103  local
   6.104  
   6.105 -rules
   6.106 +axioms
   6.107  
   6.108    (* Equality *)
   6.109  
   6.110 -  refl          "a=a"
   6.111 -  subst         "[| a=b;  P(a) |] ==> P(b)"
   6.112 +  refl:         "a=a"
   6.113 +  subst:        "[| a=b;  P(a) |] ==> P(b)"
   6.114  
   6.115    (* Propositional logic *)
   6.116  
   6.117 -  conjI         "[| P;  Q |] ==> P&Q"
   6.118 -  conjunct1     "P&Q ==> P"
   6.119 -  conjunct2     "P&Q ==> Q"
   6.120 +  conjI:        "[| P;  Q |] ==> P&Q"
   6.121 +  conjunct1:    "P&Q ==> P"
   6.122 +  conjunct2:    "P&Q ==> Q"
   6.123  
   6.124 -  disjI1        "P ==> P|Q"
   6.125 -  disjI2        "Q ==> P|Q"
   6.126 -  disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
   6.127 +  disjI1:       "P ==> P|Q"
   6.128 +  disjI2:       "Q ==> P|Q"
   6.129 +  disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
   6.130  
   6.131 -  impI          "(P ==> Q) ==> P-->Q"
   6.132 -  mp            "[| P-->Q;  P |] ==> Q"
   6.133 +  impI:         "(P ==> Q) ==> P-->Q"
   6.134 +  mp:           "[| P-->Q;  P |] ==> Q"
   6.135  
   6.136 -  FalseE        "False ==> P"
   6.137 +  FalseE:       "False ==> P"
   6.138 +
   6.139  
   6.140    (* Definitions *)
   6.141  
   6.142 -  True_def      "True  == False-->False"
   6.143 -  not_def       "~P    == P-->False"
   6.144 -  iff_def       "P<->Q == (P-->Q) & (Q-->P)"
   6.145 +  True_def:     "True  == False-->False"
   6.146 +  not_def:      "~P    == P-->False"
   6.147 +  iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
   6.148  
   6.149    (* Unique existence *)
   6.150  
   6.151 -  ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   6.152 +  ex1_def:      "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   6.153 +
   6.154  
   6.155    (* Quantifiers *)
   6.156  
   6.157 -  allI          "(!!x. P(x)) ==> (ALL x. P(x))"
   6.158 -  spec          "(ALL x. P(x)) ==> P(x)"
   6.159 +  allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
   6.160 +  spec:         "(ALL x. P(x)) ==> P(x)"
   6.161  
   6.162 -  exI           "P(x) ==> (EX x. P(x))"
   6.163 -  exE           "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   6.164 +  exI:          "P(x) ==> (EX x. P(x))"
   6.165 +  exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   6.166  
   6.167    (* Reflection *)
   6.168  
   6.169 -  eq_reflection   "(x=y)   ==> (x==y)"
   6.170 -  iff_reflection  "(P<->Q) ==> (P==Q)"
   6.171 +  eq_reflection:  "(x=y)   ==> (x==y)"
   6.172 +  iff_reflection: "(P<->Q) ==> (P==Q)"
   6.173  
   6.174  
   6.175 -setup
   6.176 -  Simplifier.setup
   6.177 +			setup Simplifier.setup
   6.178 +use "IFOL_lemmas.ML"	setup attrib_setup
   6.179 +use "fologic.ML"
   6.180 +use "hypsubstdata.ML"
   6.181 +use "intprover.ML"
   6.182 +
   6.183  
   6.184  end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/FOL/IFOL_lemmas.ML	Wed Aug 25 20:45:19 1999 +0200
     7.3 @@ -0,0 +1,480 @@
     7.4 +(*  Title:      FOL/IFOL_lemmas.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +    Copyright   1992  University of Cambridge
     7.8 +
     7.9 +Tactics and lemmas for theory IFOL (intuitionistic first-order logic).
    7.10 +*)
    7.11 +
    7.12 +(* ML bindings *)
    7.13 +
    7.14 +val refl = thm "refl";
    7.15 +val subst = thm "subst";
    7.16 +val conjI = thm "conjI";
    7.17 +val conjunct1 = thm "conjunct1";
    7.18 +val conjunct2 = thm "conjunct2";
    7.19 +val disjI1 = thm "disjI1";
    7.20 +val disjI2 = thm "disjI2";
    7.21 +val disjE = thm "disjE";
    7.22 +val impI = thm "impI";
    7.23 +val mp = thm "mp";
    7.24 +val FalseE = thm "FalseE";
    7.25 +val True_def = thm "True_def";
    7.26 +val not_def = thm "not_def";
    7.27 +val iff_def = thm "iff_def";
    7.28 +val ex1_def = thm "ex1_def";
    7.29 +val allI = thm "allI";
    7.30 +val spec = thm "spec";
    7.31 +val exI = thm "exI";
    7.32 +val exE = thm "exE";
    7.33 +val eq_reflection = thm "eq_reflection";
    7.34 +val iff_reflection = thm "iff_reflection";
    7.35 +
    7.36 +
    7.37 +
    7.38 +qed_goalw "TrueI" (the_context ()) [True_def] "True"
    7.39 + (fn _ => [ (REPEAT (ares_tac [impI] 1)) ]);
    7.40 +
    7.41 +(*** Sequent-style elimination rules for & --> and ALL ***)
    7.42 +
    7.43 +qed_goal "conjE" (the_context ()) 
    7.44 +    "[| P&Q; [| P; Q |] ==> R |] ==> R"
    7.45 + (fn prems=>
    7.46 +  [ (REPEAT (resolve_tac prems 1
    7.47 +      ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN
    7.48 +              resolve_tac prems 1))) ]);
    7.49 +
    7.50 +qed_goal "impE" (the_context ()) 
    7.51 +    "[| P-->Q;  P;  Q ==> R |] ==> R"
    7.52 + (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    7.53 +
    7.54 +qed_goal "allE" (the_context ()) 
    7.55 +    "[| ALL x. P(x); P(x) ==> R |] ==> R"
    7.56 + (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    7.57 +
    7.58 +(*Duplicates the quantifier; for use with eresolve_tac*)
    7.59 +qed_goal "all_dupE" (the_context ()) 
    7.60 +    "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R \
    7.61 +\    |] ==> R"
    7.62 + (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    7.63 +
    7.64 +
    7.65 +(*** Negation rules, which translate between ~P and P-->False ***)
    7.66 +
    7.67 +qed_goalw "notI" (the_context ()) [not_def] "(P ==> False) ==> ~P"
    7.68 + (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
    7.69 +
    7.70 +qed_goalw "notE" (the_context ()) [not_def] "[| ~P;  P |] ==> R"
    7.71 + (fn prems=>
    7.72 +  [ (resolve_tac [mp RS FalseE] 1),
    7.73 +    (REPEAT (resolve_tac prems 1)) ]);
    7.74 +
    7.75 +qed_goal "rev_notE" (the_context ()) "!!P R. [| P; ~P |] ==> R"
    7.76 + (fn _ => [REPEAT (ares_tac [notE] 1)]);
    7.77 +
    7.78 +(*This is useful with the special implication rules for each kind of P. *)
    7.79 +qed_goal "not_to_imp" (the_context ()) 
    7.80 +    "[| ~P;  (P-->False) ==> Q |] ==> Q"
    7.81 + (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
    7.82 +
    7.83 +(* For substitution into an assumption P, reduce Q to P-->Q, substitute into
    7.84 +   this implication, then apply impI to move P back into the assumptions.
    7.85 +   To specify P use something like
    7.86 +      eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
    7.87 +qed_goal "rev_mp" (the_context ()) "[| P;  P --> Q |] ==> Q"
    7.88 + (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    7.89 +
    7.90 +(*Contrapositive of an inference rule*)
    7.91 +qed_goal "contrapos" (the_context ()) "[| ~Q;  P==>Q |] ==> ~P"
    7.92 + (fn [major,minor]=> 
    7.93 +  [ (rtac (major RS notE RS notI) 1), 
    7.94 +    (etac minor 1) ]);
    7.95 +
    7.96 +
    7.97 +(*** Modus Ponens Tactics ***)
    7.98 +
    7.99 +(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   7.100 +fun mp_tac i = eresolve_tac [notE,impE] i  THEN  assume_tac i;
   7.101 +
   7.102 +(*Like mp_tac but instantiates no variables*)
   7.103 +fun eq_mp_tac i = eresolve_tac [notE,impE] i  THEN  eq_assume_tac i;
   7.104 +
   7.105 +
   7.106 +(*** If-and-only-if ***)
   7.107 +
   7.108 +qed_goalw "iffI" (the_context ()) [iff_def]
   7.109 +   "[| P ==> Q;  Q ==> P |] ==> P<->Q"
   7.110 + (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
   7.111 +
   7.112 +
   7.113 +(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   7.114 +qed_goalw "iffE" (the_context ()) [iff_def]
   7.115 +    "[| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R"
   7.116 + (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);
   7.117 +
   7.118 +(* Destruct rules for <-> similar to Modus Ponens *)
   7.119 +
   7.120 +qed_goalw "iffD1" (the_context ()) [iff_def] "[| P <-> Q;  P |] ==> Q"
   7.121 + (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   7.122 +
   7.123 +qed_goalw "iffD2" (the_context ()) [iff_def] "[| P <-> Q;  Q |] ==> P"
   7.124 + (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   7.125 +
   7.126 +qed_goal "rev_iffD1" (the_context ()) "!!P. [| P; P <-> Q |] ==> Q"
   7.127 + (fn _ => [etac iffD1 1, assume_tac 1]);
   7.128 +
   7.129 +qed_goal "rev_iffD2" (the_context ()) "!!P. [| Q; P <-> Q |] ==> P"
   7.130 + (fn _ => [etac iffD2 1, assume_tac 1]);
   7.131 +
   7.132 +qed_goal "iff_refl" (the_context ()) "P <-> P"
   7.133 + (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]);
   7.134 +
   7.135 +qed_goal "iff_sym" (the_context ()) "Q <-> P ==> P <-> Q"
   7.136 + (fn [major] =>
   7.137 +  [ (rtac (major RS iffE) 1),
   7.138 +    (rtac iffI 1),
   7.139 +    (REPEAT (eresolve_tac [asm_rl,mp] 1)) ]);
   7.140 +
   7.141 +qed_goal "iff_trans" (the_context ())
   7.142 +    "!!P Q R. [| P <-> Q;  Q<-> R |] ==> P <-> R"
   7.143 + (fn _ =>
   7.144 +  [ (rtac iffI 1),
   7.145 +    (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]);
   7.146 +
   7.147 +
   7.148 +(*** Unique existence.  NOTE THAT the following 2 quantifications
   7.149 +   EX!x such that [EX!y such that P(x,y)]     (sequential)
   7.150 +   EX!x,y such that P(x,y)                    (simultaneous)
   7.151 + do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   7.152 +***)
   7.153 +
   7.154 +qed_goalw "ex1I" (the_context ()) [ex1_def]
   7.155 +    "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)"
   7.156 + (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
   7.157 +
   7.158 +(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   7.159 +qed_goal "ex_ex1I" (the_context ())
   7.160 +    "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
   7.161 + (fn [ex,eq] => [ (rtac (ex RS exE) 1),
   7.162 +                  (REPEAT (ares_tac [ex1I,eq] 1)) ]);
   7.163 +
   7.164 +qed_goalw "ex1E" (the_context ()) [ex1_def]
   7.165 +    "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R"
   7.166 + (fn prems =>
   7.167 +  [ (cut_facts_tac prems 1),
   7.168 +    (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]);
   7.169 +
   7.170 +
   7.171 +(*** <-> congruence rules for simplification ***)
   7.172 +
   7.173 +(*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
   7.174 +fun iff_tac prems i =
   7.175 +    resolve_tac (prems RL [iffE]) i THEN
   7.176 +    REPEAT1 (eresolve_tac [asm_rl,mp] i);
   7.177 +
   7.178 +qed_goal "conj_cong" (the_context ()) 
   7.179 +    "[| P <-> P';  P' ==> Q <-> Q' |] ==> (P&Q) <-> (P'&Q')"
   7.180 + (fn prems =>
   7.181 +  [ (cut_facts_tac prems 1),
   7.182 +    (REPEAT  (ares_tac [iffI,conjI] 1
   7.183 +      ORELSE  eresolve_tac [iffE,conjE,mp] 1
   7.184 +      ORELSE  iff_tac prems 1)) ]);
   7.185 +
   7.186 +(*Reversed congruence rule!   Used in ZF/Order*)
   7.187 +qed_goal "conj_cong2" (the_context ()) 
   7.188 +    "[| P <-> P';  P' ==> Q <-> Q' |] ==> (Q&P) <-> (Q'&P')"
   7.189 + (fn prems =>
   7.190 +  [ (cut_facts_tac prems 1),
   7.191 +    (REPEAT  (ares_tac [iffI,conjI] 1
   7.192 +      ORELSE  eresolve_tac [iffE,conjE,mp] 1
   7.193 +      ORELSE  iff_tac prems 1)) ]);
   7.194 +
   7.195 +qed_goal "disj_cong" (the_context ()) 
   7.196 +    "[| P <-> P';  Q <-> Q' |] ==> (P|Q) <-> (P'|Q')"
   7.197 + (fn prems =>
   7.198 +  [ (cut_facts_tac prems 1),
   7.199 +    (REPEAT  (eresolve_tac [iffE,disjE,disjI1,disjI2] 1
   7.200 +      ORELSE  ares_tac [iffI] 1
   7.201 +      ORELSE  mp_tac 1)) ]);
   7.202 +
   7.203 +qed_goal "imp_cong" (the_context ()) 
   7.204 +    "[| P <-> P';  P' ==> Q <-> Q' |] ==> (P-->Q) <-> (P'-->Q')"
   7.205 + (fn prems =>
   7.206 +  [ (cut_facts_tac prems 1),
   7.207 +    (REPEAT   (ares_tac [iffI,impI] 1
   7.208 +      ORELSE  etac iffE 1
   7.209 +      ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
   7.210 +
   7.211 +qed_goal "iff_cong" (the_context ()) 
   7.212 +    "[| P <-> P';  Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
   7.213 + (fn prems =>
   7.214 +  [ (cut_facts_tac prems 1),
   7.215 +    (REPEAT   (etac iffE 1
   7.216 +      ORELSE  ares_tac [iffI] 1
   7.217 +      ORELSE  mp_tac 1)) ]);
   7.218 +
   7.219 +qed_goal "not_cong" (the_context ()) 
   7.220 +    "P <-> P' ==> ~P <-> ~P'"
   7.221 + (fn prems =>
   7.222 +  [ (cut_facts_tac prems 1),
   7.223 +    (REPEAT   (ares_tac [iffI,notI] 1
   7.224 +      ORELSE  mp_tac 1
   7.225 +      ORELSE  eresolve_tac [iffE,notE] 1)) ]);
   7.226 +
   7.227 +qed_goal "all_cong" (the_context ()) 
   7.228 +    "(!!x. P(x) <-> Q(x)) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
   7.229 + (fn prems =>
   7.230 +  [ (REPEAT   (ares_tac [iffI,allI] 1
   7.231 +      ORELSE   mp_tac 1
   7.232 +      ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
   7.233 +
   7.234 +qed_goal "ex_cong" (the_context ()) 
   7.235 +    "(!!x. P(x) <-> Q(x)) ==> (EX x. P(x)) <-> (EX x. Q(x))"
   7.236 + (fn prems =>
   7.237 +  [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   7.238 +      ORELSE   mp_tac 1
   7.239 +      ORELSE   iff_tac prems 1)) ]);
   7.240 +
   7.241 +qed_goal "ex1_cong" (the_context ()) 
   7.242 +    "(!!x. P(x) <-> Q(x)) ==> (EX! x. P(x)) <-> (EX! x. Q(x))"
   7.243 + (fn prems =>
   7.244 +  [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
   7.245 +      ORELSE   mp_tac 1
   7.246 +      ORELSE   iff_tac prems 1)) ]);
   7.247 +
   7.248 +(*** Equality rules ***)
   7.249 +
   7.250 +qed_goal "sym" (the_context ()) "a=b ==> b=a"
   7.251 + (fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]);
   7.252 +
   7.253 +qed_goal "trans" (the_context ()) "[| a=b;  b=c |] ==> a=c"
   7.254 + (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]);
   7.255 +
   7.256 +(** ~ b=a ==> ~ a=b **)
   7.257 +val [not_sym] = compose(sym,2,contrapos);
   7.258 +
   7.259 +
   7.260 +(* Two theorms for rewriting only one instance of a definition:
   7.261 +   the first for definitions of formulae and the second for terms *)
   7.262 +
   7.263 +val prems = goal (the_context ()) "(A == B) ==> A <-> B";
   7.264 +by (rewrite_goals_tac prems);
   7.265 +by (rtac iff_refl 1);
   7.266 +qed "def_imp_iff";
   7.267 +
   7.268 +val prems = goal (the_context ()) "(A == B) ==> A = B";
   7.269 +by (rewrite_goals_tac prems);
   7.270 +by (rtac refl 1);
   7.271 +qed "meta_eq_to_obj_eq";
   7.272 +
   7.273 +
   7.274 +(*Substitution: rule and tactic*)
   7.275 +bind_thm ("ssubst", sym RS subst);
   7.276 +
   7.277 +(*Apply an equality or definition ONCE.
   7.278 +  Fails unless the substitution has an effect*)
   7.279 +fun stac th = 
   7.280 +  let val th' = th RS meta_eq_to_obj_eq handle THM _ => th
   7.281 +  in  CHANGED_GOAL (rtac (th' RS ssubst))
   7.282 +  end;
   7.283 +
   7.284 +(*A special case of ex1E that would otherwise need quantifier expansion*)
   7.285 +qed_goal "ex1_equalsE" (the_context ())
   7.286 +    "[| EX! x. P(x);  P(a);  P(b) |] ==> a=b"
   7.287 + (fn prems =>
   7.288 +  [ (cut_facts_tac prems 1),
   7.289 +    (etac ex1E 1),
   7.290 +    (rtac trans 1),
   7.291 +    (rtac sym 2),
   7.292 +    (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]);
   7.293 +
   7.294 +(** Polymorphic congruence rules **)
   7.295 +
   7.296 +qed_goal "subst_context" (the_context ()) 
   7.297 +   "[| a=b |]  ==>  t(a)=t(b)"
   7.298 + (fn prems=>
   7.299 +  [ (resolve_tac (prems RL [ssubst]) 1),
   7.300 +    (rtac refl 1) ]);
   7.301 +
   7.302 +qed_goal "subst_context2" (the_context ()) 
   7.303 +   "[| a=b;  c=d |]  ==>  t(a,c)=t(b,d)"
   7.304 + (fn prems=>
   7.305 +  [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   7.306 +
   7.307 +qed_goal "subst_context3" (the_context ()) 
   7.308 +   "[| a=b;  c=d;  e=f |]  ==>  t(a,c,e)=t(b,d,f)"
   7.309 + (fn prems=>
   7.310 +  [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   7.311 +
   7.312 +(*Useful with eresolve_tac for proving equalties from known equalities.
   7.313 +        a = b
   7.314 +        |   |
   7.315 +        c = d   *)
   7.316 +qed_goal "box_equals" (the_context ())
   7.317 +    "[| a=b;  a=c;  b=d |] ==> c=d"  
   7.318 + (fn prems=>
   7.319 +  [ (rtac trans 1),
   7.320 +    (rtac trans 1),
   7.321 +    (rtac sym 1),
   7.322 +    (REPEAT (resolve_tac prems 1)) ]);
   7.323 +
   7.324 +(*Dual of box_equals: for proving equalities backwards*)
   7.325 +qed_goal "simp_equals" (the_context ())
   7.326 +    "[| a=c;  b=d;  c=d |] ==> a=b"  
   7.327 + (fn prems=>
   7.328 +  [ (rtac trans 1),
   7.329 +    (rtac trans 1),
   7.330 +    (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]);
   7.331 +
   7.332 +(** Congruence rules for predicate letters **)
   7.333 +
   7.334 +qed_goal "pred1_cong" (the_context ())
   7.335 +    "a=a' ==> P(a) <-> P(a')"
   7.336 + (fn prems =>
   7.337 +  [ (cut_facts_tac prems 1),
   7.338 +    (rtac iffI 1),
   7.339 +    (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   7.340 +
   7.341 +qed_goal "pred2_cong" (the_context ())
   7.342 +    "[| a=a';  b=b' |] ==> P(a,b) <-> P(a',b')"
   7.343 + (fn prems =>
   7.344 +  [ (cut_facts_tac prems 1),
   7.345 +    (rtac iffI 1),
   7.346 +    (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   7.347 +
   7.348 +qed_goal "pred3_cong" (the_context ())
   7.349 +    "[| a=a';  b=b';  c=c' |] ==> P(a,b,c) <-> P(a',b',c')"
   7.350 + (fn prems =>
   7.351 +  [ (cut_facts_tac prems 1),
   7.352 +    (rtac iffI 1),
   7.353 +    (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   7.354 +
   7.355 +(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   7.356 +
   7.357 +val pred_congs = 
   7.358 +    flat (map (fn c => 
   7.359 +               map (fn th => read_instantiate [("P",c)] th)
   7.360 +                   [pred1_cong,pred2_cong,pred3_cong])
   7.361 +               (explode"PQRS"));
   7.362 +
   7.363 +(*special case for the equality predicate!*)
   7.364 +val eq_cong = read_instantiate [("P","op =")] pred2_cong;
   7.365 +
   7.366 +
   7.367 +(*** Simplifications of assumed implications.
   7.368 +     Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
   7.369 +     used with mp_tac (restricted to atomic formulae) is COMPLETE for 
   7.370 +     intuitionistic propositional logic.  See
   7.371 +   R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   7.372 +    (preprint, University of St Andrews, 1991)  ***)
   7.373 +
   7.374 +qed_goal "conj_impE" (the_context ()) 
   7.375 +    "[| (P&Q)-->S;  P-->(Q-->S) ==> R |] ==> R"
   7.376 + (fn major::prems=>
   7.377 +  [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
   7.378 +
   7.379 +qed_goal "disj_impE" (the_context ()) 
   7.380 +    "[| (P|Q)-->S;  [| P-->S; Q-->S |] ==> R |] ==> R"
   7.381 + (fn major::prems=>
   7.382 +  [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]);
   7.383 +
   7.384 +(*Simplifies the implication.  Classical version is stronger. 
   7.385 +  Still UNSAFE since Q must be provable -- backtracking needed.  *)
   7.386 +qed_goal "imp_impE" (the_context ()) 
   7.387 +    "[| (P-->Q)-->S;  [| P; Q-->S |] ==> Q;  S ==> R |] ==> R"
   7.388 + (fn major::prems=>
   7.389 +  [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
   7.390 +
   7.391 +(*Simplifies the implication.  Classical version is stronger. 
   7.392 +  Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   7.393 +qed_goal "not_impE" (the_context ())
   7.394 +    "[| ~P --> S;  P ==> False;  S ==> R |] ==> R"
   7.395 + (fn major::prems=>
   7.396 +  [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
   7.397 +
   7.398 +(*Simplifies the implication.   UNSAFE.  *)
   7.399 +qed_goal "iff_impE" (the_context ()) 
   7.400 +    "[| (P<->Q)-->S;  [| P; Q-->S |] ==> Q;  [| Q; P-->S |] ==> P;  \
   7.401 +\       S ==> R |] ==> R"
   7.402 + (fn major::prems=>
   7.403 +  [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
   7.404 +
   7.405 +(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   7.406 +qed_goal "all_impE" (the_context ()) 
   7.407 +    "[| (ALL x. P(x))-->S;  !!x. P(x);  S ==> R |] ==> R"
   7.408 + (fn major::prems=>
   7.409 +  [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
   7.410 +
   7.411 +(*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   7.412 +qed_goal "ex_impE" (the_context ()) 
   7.413 +    "[| (EX x. P(x))-->S;  P(x)-->S ==> R |] ==> R"
   7.414 + (fn major::prems=>
   7.415 +  [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
   7.416 +
   7.417 +(*** Courtesy of Krzysztof Grabczewski ***)
   7.418 +
   7.419 +val major::prems = goal (the_context ()) "[| P|Q;  P==>R;  Q==>S |] ==> R|S";
   7.420 +by (rtac (major RS disjE) 1);
   7.421 +by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
   7.422 +qed "disj_imp_disj";
   7.423 +
   7.424 +
   7.425 +(** strip ALL and --> from proved goal while preserving ALL-bound var names **)
   7.426 +
   7.427 +fun make_new_spec rl =
   7.428 +  (* Use a crazy name to avoid forall_intr failing because of
   7.429 +     duplicate variable name *)
   7.430 +  let val myspec = read_instantiate [("P","?wlzickd")] rl
   7.431 +      val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
   7.432 +      val cvx = cterm_of (#sign(rep_thm myspec)) vx
   7.433 +  in (vxT, forall_intr cvx myspec) end;
   7.434 +
   7.435 +local
   7.436 +
   7.437 +val (specT,  spec')  = make_new_spec spec
   7.438 +
   7.439 +in
   7.440 +
   7.441 +fun RSspec th =
   7.442 +  (case concl_of th of
   7.443 +     _ $ (Const("All",_) $ Abs(a,_,_)) =>
   7.444 +         let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT))
   7.445 +         in th RS forall_elim ca spec' end
   7.446 +  | _ => raise THM("RSspec",0,[th]));
   7.447 +
   7.448 +fun RSmp th =
   7.449 +  (case concl_of th of
   7.450 +     _ $ (Const("op -->",_)$_$_) => th RS mp
   7.451 +  | _ => raise THM("RSmp",0,[th]));
   7.452 +
   7.453 +fun normalize_thm funs =
   7.454 +  let fun trans [] th = th
   7.455 +	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   7.456 +  in trans funs end;
   7.457 +
   7.458 +fun qed_spec_mp name =
   7.459 +  let val thm = normalize_thm [RSspec,RSmp] (result())
   7.460 +  in bind_thm(name, thm) end;
   7.461 +
   7.462 +fun qed_goal_spec_mp name thy s p = 
   7.463 +      bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   7.464 +
   7.465 +fun qed_goalw_spec_mp name thy defs s p = 
   7.466 +      bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   7.467 +
   7.468 +end;
   7.469 +
   7.470 +
   7.471 +(* attributes *)
   7.472 +
   7.473 +local
   7.474 +
   7.475 +fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
   7.476 +
   7.477 +in
   7.478 +
   7.479 +val attrib_setup =
   7.480 + [Attrib.add_attributes
   7.481 +  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
   7.482 +
   7.483 +end;
     8.1 --- a/src/FOL/IsaMakefile	Wed Aug 25 20:42:01 1999 +0200
     8.2 +++ b/src/FOL/IsaMakefile	Wed Aug 25 20:45:19 1999 +0200
     8.3 @@ -30,8 +30,9 @@
     8.4    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
     8.5    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML \
     8.6    $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML FOL.ML \
     8.7 -  FOL.thy IFOL.ML IFOL.thy ROOT.ML cladata.ML fologic.ML intprover.ML \
     8.8 -  simpdata.ML
     8.9 +  FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \
    8.10 +  IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML fologic.ML \
    8.11 +  hypsubstdata.ML intprover.ML simpdata.ML
    8.12  	@$(ISATOOL) usedir -b $(OUT)/Pure FOL
    8.13  
    8.14  
     9.1 --- a/src/FOL/ROOT.ML	Wed Aug 25 20:42:01 1999 +0200
     9.2 +++ b/src/FOL/ROOT.ML	Wed Aug 25 20:45:19 1999 +0200
     9.3 @@ -1,10 +1,9 @@
     9.4 -(*  Title:      FOL/ROOT
     9.5 +(*  Title:      FOL/ROOT.ML
     9.6      ID:         $Id$
     9.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.8      Copyright   1993  University of Cambridge
     9.9  
    9.10 -Adds First-Order Logic to a database containing pure Isabelle. 
    9.11 -Should be executed in the subdirectory FOL.
    9.12 +First-Order Logic.
    9.13  *)
    9.14  
    9.15  val banner = "First-Order Logic with Natural Deduction";
    9.16 @@ -23,39 +22,6 @@
    9.17  use "~~/src/Provers/quantifier1.ML";
    9.18  
    9.19  use_thy "IFOL";
    9.20 -use "fologic.ML";
    9.21 -
    9.22 -(** Applying HypsubstFun to generate hyp_subst_tac **)
    9.23 -structure Hypsubst_Data =
    9.24 -  struct
    9.25 -  structure Simplifier = Simplifier
    9.26 -    (*These destructors  Match!*)
    9.27 -  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
    9.28 -  val dest_Trueprop = FOLogic.dest_Trueprop
    9.29 -  val dest_imp = FOLogic.dest_imp
    9.30 -  val eq_reflection = eq_reflection
    9.31 -  val imp_intr = impI
    9.32 -  val rev_mp = rev_mp
    9.33 -  val subst = subst
    9.34 -  val sym = sym
    9.35 -  val thin_refl = prove_goal IFOL.thy 
    9.36 -		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
    9.37 -  end;
    9.38 -
    9.39 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    9.40 -open Hypsubst;
    9.41 -
    9.42 -
    9.43 -use "intprover.ML";
    9.44 -
    9.45  use_thy "FOL";
    9.46  
    9.47 -use "cladata.ML";
    9.48 -use "simpdata.ML";
    9.49 -
    9.50 -qed_goal "ex1_functional" FOL.thy
    9.51 -    "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
    9.52 - (fn _ => [ (Blast_tac 1) ]);
    9.53 -
    9.54 -
    9.55  print_depth 8;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/FOL/blastdata.ML	Wed Aug 25 20:45:19 1999 +0200
    10.3 @@ -0,0 +1,20 @@
    10.4 +
    10.5 +(*** Applying BlastFun to create Blast_tac ***)
    10.6 +structure Blast_Data = 
    10.7 +  struct
    10.8 +  type claset	= Cla.claset
    10.9 +  val notE	= notE
   10.10 +  val ccontr	= ccontr
   10.11 +  val contr_tac = Cla.contr_tac
   10.12 +  val dup_intr	= Cla.dup_intr
   10.13 +  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   10.14 +  val claset	= Cla.claset
   10.15 +  val rep_cs    = Cla.rep_cs
   10.16 +  val cla_modifiers = Cla.cla_modifiers;
   10.17 +  val cla_meth' = Cla.cla_meth'
   10.18 +  end;
   10.19 +
   10.20 +structure Blast = BlastFun(Blast_Data);
   10.21 +
   10.22 +val Blast_tac = Blast.Blast_tac
   10.23 +and blast_tac = Blast.blast_tac;
    11.1 --- a/src/FOL/cladata.ML	Wed Aug 25 20:42:01 1999 +0200
    11.2 +++ b/src/FOL/cladata.ML	Wed Aug 25 20:45:19 1999 +0200
    11.3 @@ -3,10 +3,9 @@
    11.4      Author:     Tobias Nipkow
    11.5      Copyright   1996  University of Cambridge
    11.6  
    11.7 -Setting up the classical reasoner 
    11.8 +Setting up the classical reasoner.
    11.9  *)
   11.10  
   11.11 -
   11.12  section "Classical Reasoner";
   11.13  
   11.14  
   11.15 @@ -24,6 +23,7 @@
   11.16  structure BasicClassical: BASIC_CLASSICAL = Cla;
   11.17  open BasicClassical;
   11.18  
   11.19 +
   11.20  (*Better for fast_tac: needs no quantifier duplication!*)
   11.21  qed_goal "alt_ex1E" IFOL.thy
   11.22      "[| EX! x. P(x);                                              \
   11.23 @@ -44,25 +44,4 @@
   11.24  val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
   11.25                       addSEs [exE,alt_ex1E] addEs [allE];
   11.26  
   11.27 -claset_ref() := FOL_cs;
   11.28 -
   11.29 -
   11.30 -(*** Applying BlastFun to create Blast_tac ***)
   11.31 -structure Blast_Data = 
   11.32 -  struct
   11.33 -  type claset	= Cla.claset
   11.34 -  val notE	= notE
   11.35 -  val ccontr	= ccontr
   11.36 -  val contr_tac = Cla.contr_tac
   11.37 -  val dup_intr	= Cla.dup_intr
   11.38 -  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   11.39 -  val claset	= Cla.claset
   11.40 -  val rep_cs    = Cla.rep_cs
   11.41 -  val cla_modifiers = Cla.cla_modifiers;
   11.42 -  val cla_meth' = Cla.cla_meth'
   11.43 -  end;
   11.44 -
   11.45 -structure Blast = BlastFun(Blast_Data);
   11.46 -
   11.47 -val Blast_tac = Blast.Blast_tac
   11.48 -and blast_tac = Blast.blast_tac;
   11.49 +val clasetup = [fn thy => (claset_ref_of thy := FOL_cs; thy)];
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/FOL/hypsubstdata.ML	Wed Aug 25 20:45:19 1999 +0200
    12.3 @@ -0,0 +1,20 @@
    12.4 +
    12.5 +(** Applying HypsubstFun to generate hyp_subst_tac **)
    12.6 +structure Hypsubst_Data =
    12.7 +  struct
    12.8 +  structure Simplifier = Simplifier
    12.9 +    (*These destructors  Match!*)
   12.10 +  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
   12.11 +  val dest_Trueprop = FOLogic.dest_Trueprop
   12.12 +  val dest_imp = FOLogic.dest_imp
   12.13 +  val eq_reflection = eq_reflection
   12.14 +  val imp_intr = impI
   12.15 +  val rev_mp = rev_mp
   12.16 +  val subst = subst
   12.17 +  val sym = sym
   12.18 +  val thin_refl = prove_goal (the_context ())
   12.19 +		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
   12.20 +  end;
   12.21 +
   12.22 +structure Hypsubst = HypsubstFun(Hypsubst_Data);
   12.23 +open Hypsubst;
    13.1 --- a/src/FOL/simpdata.ML	Wed Aug 25 20:42:01 1999 +0200
    13.2 +++ b/src/FOL/simpdata.ML	Wed Aug 25 20:45:19 1999 +0200
    13.3 @@ -127,7 +127,7 @@
    13.4  
    13.5  fun prove_fun s = 
    13.6   (writeln s;  
    13.7 -  prove_goal FOL.thy s
    13.8 +  prove_goal (the_context ()) s
    13.9     (fn prems => [ (cut_facts_tac prems 1), 
   13.10                    (Cla.fast_tac FOL_cs 1) ]));
   13.11  
   13.12 @@ -177,7 +177,7 @@
   13.13      (fn prems => [ (cut_facts_tac prems 1), 
   13.14                     (IntPr.fast_tac 1) ]);
   13.15  
   13.16 -fun prove nm thm  = qed_goal nm FOL.thy thm (fn _ => [Blast_tac 1]);
   13.17 +fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [Blast_tac 1]);
   13.18  
   13.19  int_prove "conj_commute" "P&Q <-> Q&P";
   13.20  int_prove "conj_left_commute" "P&(Q&R) <-> Q&(P&R)";
   13.21 @@ -242,11 +242,12 @@
   13.22  end);
   13.23  
   13.24  local
   13.25 +
   13.26  val ex_pattern =
   13.27 -  read_cterm (Theory.sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
   13.28 +  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
   13.29  
   13.30  val all_pattern =
   13.31 -  read_cterm (Theory.sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
   13.32 +  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
   13.33  
   13.34  in
   13.35  val defEX_regroup =
   13.36 @@ -348,8 +349,7 @@
   13.37  (*classical simprules too*)
   13.38  val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
   13.39  
   13.40 -simpset_ref() := FOL_ss;
   13.41 -
   13.42 +val simpsetup = [fn thy => (simpset_ref_of thy := FOL_ss; thy)];
   13.43  
   13.44  
   13.45  (*** integration of simplifier with classical reasoner ***)