src/FOLP/IFOLP.thy
author wenzelm
Wed Jun 11 18:01:36 2008 +0200 (2008-06-11)
changeset 27152 192954a9a549
parent 27150 a42aef558ce3
child 29269 5c25a2012975
permissions -rw-r--r--
changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
     1 (*  Title:      FOLP/IFOLP.thy
     2     ID:         $Id$
     3     Author:     Martin D Coen, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 *)
     6 
     7 header {* Intuitionistic First-Order Logic with Proofs *}
     8 
     9 theory IFOLP
    10 imports Pure
    11 uses ("hypsubst.ML") ("intprover.ML")
    12 begin
    13 
    14 setup PureThy.old_appl_syntax_setup
    15 
    16 global
    17 
    18 classes "term"
    19 defaultsort "term"
    20 
    21 typedecl p
    22 typedecl o
    23 
    24 consts
    25       (*** Judgements ***)
    26  "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
    27  Proof          ::   "[o,p]=>prop"
    28  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    29 
    30       (*** Logical Connectives -- Type Formers ***)
    31  "="            ::      "['a,'a] => o"  (infixl 50)
    32  True           ::      "o"
    33  False          ::      "o"
    34  Not            ::      "o => o"        ("~ _" [40] 40)
    35  "&"            ::      "[o,o] => o"    (infixr 35)
    36  "|"            ::      "[o,o] => o"    (infixr 30)
    37  "-->"          ::      "[o,o] => o"    (infixr 25)
    38  "<->"          ::      "[o,o] => o"    (infixr 25)
    39       (*Quantifiers*)
    40  All            ::      "('a => o) => o"        (binder "ALL " 10)
    41  Ex             ::      "('a => o) => o"        (binder "EX " 10)
    42  Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
    43       (*Rewriting gadgets*)
    44  NORM           ::      "o => o"
    45  norm           ::      "'a => 'a"
    46 
    47       (*** Proof Term Formers: precedence must exceed 50 ***)
    48  tt             :: "p"
    49  contr          :: "p=>p"
    50  fst            :: "p=>p"
    51  snd            :: "p=>p"
    52  pair           :: "[p,p]=>p"           ("(1<_,/_>)")
    53  split          :: "[p, [p,p]=>p] =>p"
    54  inl            :: "p=>p"
    55  inr            :: "p=>p"
    56  when           :: "[p, p=>p, p=>p]=>p"
    57  lambda         :: "(p => p) => p"      (binder "lam " 55)
    58  "`"            :: "[p,p]=>p"           (infixl 60)
    59  alll           :: "['a=>p]=>p"         (binder "all " 55)
    60  "^"            :: "[p,'a]=>p"          (infixl 55)
    61  exists         :: "['a,p]=>p"          ("(1[_,/_])")
    62  xsplit         :: "[p,['a,p]=>p]=>p"
    63  ideq           :: "'a=>p"
    64  idpeel         :: "[p,'a=>p]=>p"
    65  nrm            :: p
    66  NRM            :: p
    67 
    68 local
    69 
    70 ML {*
    71 
    72 (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
    73 val show_proofs = ref false;
    74 
    75 fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) $ P $ p;
    76 
    77 fun proof_tr' [P,p] =
    78     if !show_proofs then Const("@Proof",dummyT) $ p $ P
    79     else P  (*this case discards the proof term*);
    80 *}
    81 
    82 parse_translation {* [("@Proof", proof_tr)] *}
    83 print_translation {* [("Proof", proof_tr')] *}
    84 
    85 axioms
    86 
    87 (**** Propositional logic ****)
    88 
    89 (*Equality*)
    90 (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
    91 
    92 ieqI:      "ideq(a) : a=a"
    93 ieqE:      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    94 
    95 (* Truth and Falsity *)
    96 
    97 TrueI:     "tt : True"
    98 FalseE:    "a:False ==> contr(a):P"
    99 
   100 (* Conjunction *)
   101 
   102 conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
   103 conjunct1: "p:P&Q ==> fst(p):P"
   104 conjunct2: "p:P&Q ==> snd(p):Q"
   105 
   106 (* Disjunction *)
   107 
   108 disjI1:    "a:P ==> inl(a):P|Q"
   109 disjI2:    "b:Q ==> inr(b):P|Q"
   110 disjE:     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R
   111            |] ==> when(a,f,g):R"
   112 
   113 (* Implication *)
   114 
   115 impI:      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
   116 mp:        "[| f:P-->Q;  a:P |] ==> f`a:Q"
   117 
   118 (*Quantifiers*)
   119 
   120 allI:      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
   121 spec:      "(f:ALL x. P(x)) ==> f^x : P(x)"
   122 
   123 exI:       "p : P(x) ==> [x,p] : EX x. P(x)"
   124 exE:       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
   125 
   126 (**** Equality between proofs ****)
   127 
   128 prefl:     "a : P ==> a = a : P"
   129 psym:      "a = b : P ==> b = a : P"
   130 ptrans:    "[| a = b : P;  b = c : P |] ==> a = c : P"
   131 
   132 idpeelB:   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
   133 
   134 fstB:      "a:P ==> fst(<a,b>) = a : P"
   135 sndB:      "b:Q ==> snd(<a,b>) = b : Q"
   136 pairEC:    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
   137 
   138 whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
   139 whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
   140 plusEC:    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
   141 
   142 applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
   143 funEC:      "f:P ==> f = lam x. f`x : P"
   144 
   145 specB:      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
   146 
   147 
   148 (**** Definitions ****)
   149 
   150 not_def:              "~P == P-->False"
   151 iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
   152 
   153 (*Unique existence*)
   154 ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   155 
   156 (*Rewriting -- special constants to flag normalized terms and formulae*)
   157 norm_eq: "nrm : norm(x) = x"
   158 NORM_iff:        "NRM : NORM(P) <-> P"
   159 
   160 (*** Sequent-style elimination rules for & --> and ALL ***)
   161 
   162 lemma conjE:
   163   assumes "p:P&Q"
   164     and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
   165   shows "?a:R"
   166   apply (rule assms(2))
   167    apply (rule conjunct1 [OF assms(1)])
   168   apply (rule conjunct2 [OF assms(1)])
   169   done
   170 
   171 lemma impE:
   172   assumes "p:P-->Q"
   173     and "q:P"
   174     and "!!x. x:Q ==> r(x):R"
   175   shows "?p:R"
   176   apply (rule assms mp)+
   177   done
   178 
   179 lemma allE:
   180   assumes "p:ALL x. P(x)"
   181     and "!!y. y:P(x) ==> q(y):R"
   182   shows "?p:R"
   183   apply (rule assms spec)+
   184   done
   185 
   186 (*Duplicates the quantifier; for use with eresolve_tac*)
   187 lemma all_dupE:
   188   assumes "p:ALL x. P(x)"
   189     and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
   190   shows "?p:R"
   191   apply (rule assms spec)+
   192   done
   193 
   194 
   195 (*** Negation rules, which translate between ~P and P-->False ***)
   196 
   197 lemma notI:
   198   assumes "!!x. x:P ==> q(x):False"
   199   shows "?p:~P"
   200   unfolding not_def
   201   apply (assumption | rule assms impI)+
   202   done
   203 
   204 lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
   205   unfolding not_def
   206   apply (drule (1) mp)
   207   apply (erule FalseE)
   208   done
   209 
   210 (*This is useful with the special implication rules for each kind of P. *)
   211 lemma not_to_imp:
   212   assumes "p:~P"
   213     and "!!x. x:(P-->False) ==> q(x):Q"
   214   shows "?p:Q"
   215   apply (assumption | rule assms impI notE)+
   216   done
   217 
   218 (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
   219    this implication, then apply impI to move P back into the assumptions.*)
   220 lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
   221   apply (assumption | rule mp)+
   222   done
   223 
   224 
   225 (*Contrapositive of an inference rule*)
   226 lemma contrapos:
   227   assumes major: "p:~Q"
   228     and minor: "!!y. y:P==>q(y):Q"
   229   shows "?a:~P"
   230   apply (rule major [THEN notE, THEN notI])
   231   apply (erule minor)
   232   done
   233 
   234 (** Unique assumption tactic.
   235     Ignores proof objects.
   236     Fails unless one assumption is equal and exactly one is unifiable
   237 **)
   238 
   239 ML {*
   240 local
   241   fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P;
   242 in
   243 val uniq_assume_tac =
   244   SUBGOAL
   245     (fn (prem,i) =>
   246       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
   247           and concl = discard_proof (Logic.strip_assums_concl prem)
   248       in
   249           if exists (fn hyp => hyp aconv concl) hyps
   250           then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
   251                    [_] => assume_tac i
   252                  |  _  => no_tac
   253           else no_tac
   254       end);
   255 end;
   256 *}
   257 
   258 
   259 (*** Modus Ponens Tactics ***)
   260 
   261 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   262 ML {*
   263   fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac i
   264 *}
   265 
   266 (*Like mp_tac but instantiates no variables*)
   267 ML {*
   268   fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  uniq_assume_tac i
   269 *}
   270 
   271 
   272 (*** If-and-only-if ***)
   273 
   274 lemma iffI:
   275   assumes "!!x. x:P ==> q(x):Q"
   276     and "!!x. x:Q ==> r(x):P"
   277   shows "?p:P<->Q"
   278   unfolding iff_def
   279   apply (assumption | rule assms conjI impI)+
   280   done
   281 
   282 
   283 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   284   
   285 lemma iffE:
   286   assumes "p:P <-> Q"
   287     and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
   288   shows "?p:R"
   289   apply (rule conjE)
   290    apply (rule assms(1) [unfolded iff_def])
   291   apply (rule assms(2))
   292    apply assumption+
   293   done
   294 
   295 (* Destruct rules for <-> similar to Modus Ponens *)
   296 
   297 lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
   298   unfolding iff_def
   299   apply (rule conjunct1 [THEN mp], assumption+)
   300   done
   301 
   302 lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
   303   unfolding iff_def
   304   apply (rule conjunct2 [THEN mp], assumption+)
   305   done
   306 
   307 lemma iff_refl: "?p:P <-> P"
   308   apply (rule iffI)
   309    apply assumption+
   310   done
   311 
   312 lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
   313   apply (erule iffE)
   314   apply (rule iffI)
   315    apply (erule (1) mp)+
   316   done
   317 
   318 lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
   319   apply (rule iffI)
   320    apply (assumption | erule iffE | erule (1) impE)+
   321   done
   322 
   323 (*** Unique existence.  NOTE THAT the following 2 quantifications
   324    EX!x such that [EX!y such that P(x,y)]     (sequential)
   325    EX!x,y such that P(x,y)                    (simultaneous)
   326  do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   327 ***)
   328 
   329 lemma ex1I:
   330   assumes "p:P(a)"
   331     and "!!x u. u:P(x) ==> f(u) : x=a"
   332   shows "?p:EX! x. P(x)"
   333   unfolding ex1_def
   334   apply (assumption | rule assms exI conjI allI impI)+
   335   done
   336 
   337 lemma ex1E:
   338   assumes "p:EX! x. P(x)"
   339     and "!!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
   340   shows "?a : R"
   341   apply (insert assms(1) [unfolded ex1_def])
   342   apply (erule exE conjE | assumption | rule assms(1))+
   343   done
   344 
   345 
   346 (*** <-> congruence rules for simplification ***)
   347 
   348 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
   349 ML {*
   350 fun iff_tac prems i =
   351     resolve_tac (prems RL [@{thm iffE}]) i THEN
   352     REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i)
   353 *}
   354 
   355 lemma conj_cong:
   356   assumes "p:P <-> P'"
   357     and "!!x. x:P' ==> q(x):Q <-> Q'"
   358   shows "?p:(P&Q) <-> (P'&Q')"
   359   apply (insert assms(1))
   360   apply (assumption | rule iffI conjI |
   361     erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
   362   done
   363 
   364 lemma disj_cong:
   365   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
   366   apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
   367   done
   368 
   369 lemma imp_cong:
   370   assumes "p:P <-> P'"
   371     and "!!x. x:P' ==> q(x):Q <-> Q'"
   372   shows "?p:(P-->Q) <-> (P'-->Q')"
   373   apply (insert assms(1))
   374   apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} |
   375     tactic {* iff_tac @{thms assms} 1 *})+
   376   done
   377 
   378 lemma iff_cong:
   379   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
   380   apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
   381   done
   382 
   383 lemma not_cong:
   384   "p:P <-> P' ==> ?p:~P <-> ~P'"
   385   apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
   386   done
   387 
   388 lemma all_cong:
   389   assumes "!!x. f(x):P(x) <-> Q(x)"
   390   shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
   391   apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
   392     tactic {* iff_tac @{thms assms} 1 *})+
   393   done
   394 
   395 lemma ex_cong:
   396   assumes "!!x. f(x):P(x) <-> Q(x)"
   397   shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
   398   apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
   399     tactic {* iff_tac @{thms assms} 1 *})+
   400   done
   401 
   402 (*NOT PROVED
   403 bind_thm ("ex1_cong", prove_goal (the_context ())
   404     "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
   405  (fn prems =>
   406   [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
   407       ORELSE   mp_tac 1
   408       ORELSE   iff_tac prems 1)) ]))
   409 *)
   410 
   411 (*** Equality rules ***)
   412 
   413 lemmas refl = ieqI
   414 
   415 lemma subst:
   416   assumes prem1: "p:a=b"
   417     and prem2: "q:P(a)"
   418   shows "?p : P(b)"
   419   apply (rule prem2 [THEN rev_mp])
   420   apply (rule prem1 [THEN ieqE])
   421   apply (rule impI)
   422   apply assumption
   423   done
   424 
   425 lemma sym: "q:a=b ==> ?c:b=a"
   426   apply (erule subst)
   427   apply (rule refl)
   428   done
   429 
   430 lemma trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
   431   apply (erule (1) subst)
   432   done
   433 
   434 (** ~ b=a ==> ~ a=b **)
   435 lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
   436   apply (erule contrapos)
   437   apply (erule sym)
   438   done
   439 
   440 (*calling "standard" reduces maxidx to 0*)
   441 lemmas ssubst = sym [THEN subst, standard]
   442 
   443 (*A special case of ex1E that would otherwise need quantifier expansion*)
   444 lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
   445   apply (erule ex1E)
   446   apply (rule trans)
   447    apply (rule_tac [2] sym)
   448    apply (assumption | erule spec [THEN mp])+
   449   done
   450 
   451 (** Polymorphic congruence rules **)
   452 
   453 lemma subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
   454   apply (erule ssubst)
   455   apply (rule refl)
   456   done
   457 
   458 lemma subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
   459   apply (erule ssubst)+
   460   apply (rule refl)
   461   done
   462 
   463 lemma subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
   464   apply (erule ssubst)+
   465   apply (rule refl)
   466   done
   467 
   468 (*Useful with eresolve_tac for proving equalties from known equalities.
   469         a = b
   470         |   |
   471         c = d   *)
   472 lemma box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
   473   apply (rule trans)
   474    apply (rule trans)
   475     apply (rule sym)
   476     apply assumption+
   477   done
   478 
   479 (*Dual of box_equals: for proving equalities backwards*)
   480 lemma simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
   481   apply (rule trans)
   482    apply (rule trans)
   483     apply (assumption | rule sym)+
   484   done
   485 
   486 (** Congruence rules for predicate letters **)
   487 
   488 lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
   489   apply (rule iffI)
   490    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   491   done
   492 
   493 lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
   494   apply (rule iffI)
   495    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   496   done
   497 
   498 lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
   499   apply (rule iffI)
   500    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
   501   done
   502 
   503 lemmas pred_congs = pred1_cong pred2_cong pred3_cong
   504 
   505 (*special case for the equality predicate!*)
   506 lemmas eq_cong = pred2_cong [where P = "op =", standard]
   507 
   508 
   509 (*** Simplifications of assumed implications.
   510      Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
   511      used with mp_tac (restricted to atomic formulae) is COMPLETE for
   512      intuitionistic propositional logic.  See
   513    R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   514     (preprint, University of St Andrews, 1991)  ***)
   515 
   516 lemma conj_impE:
   517   assumes major: "p:(P&Q)-->S"
   518     and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
   519   shows "?p:R"
   520   apply (assumption | rule conjI impI major [THEN mp] minor)+
   521   done
   522 
   523 lemma disj_impE:
   524   assumes major: "p:(P|Q)-->S"
   525     and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
   526   shows "?p:R"
   527   apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
   528       resolve_tac [@{thm disjI1}, @{thm disjI2}, @{thm impI},
   529         @{thm major} RS @{thm mp}, @{thm minor}] 1) *})
   530   done
   531 
   532 (*Simplifies the implication.  Classical version is stronger.
   533   Still UNSAFE since Q must be provable -- backtracking needed.  *)
   534 lemma imp_impE:
   535   assumes major: "p:(P-->Q)-->S"
   536     and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
   537     and r2: "!!x. x:S ==> r(x):R"
   538   shows "?p:R"
   539   apply (assumption | rule impI major [THEN mp] r1 r2)+
   540   done
   541 
   542 (*Simplifies the implication.  Classical version is stronger.
   543   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   544 lemma not_impE:
   545   assumes major: "p:~P --> S"
   546     and r1: "!!y. y:P ==> q(y):False"
   547     and r2: "!!y. y:S ==> r(y):R"
   548   shows "?p:R"
   549   apply (assumption | rule notI impI major [THEN mp] r1 r2)+
   550   done
   551 
   552 (*Simplifies the implication.   UNSAFE.  *)
   553 lemma iff_impE:
   554   assumes major: "p:(P<->Q)-->S"
   555     and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
   556     and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
   557     and r3: "!!x. x:S ==> s(x):R"
   558   shows "?p:R"
   559   apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
   560   done
   561 
   562 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   563 lemma all_impE:
   564   assumes major: "p:(ALL x. P(x))-->S"
   565     and r1: "!!x. q:P(x)"
   566     and r2: "!!y. y:S ==> r(y):R"
   567   shows "?p:R"
   568   apply (assumption | rule allI impI major [THEN mp] r1 r2)+
   569   done
   570 
   571 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   572 lemma ex_impE:
   573   assumes major: "p:(EX x. P(x))-->S"
   574     and r: "!!y. y:P(a)-->S ==> q(y):R"
   575   shows "?p:R"
   576   apply (assumption | rule exI impI major [THEN mp] r)+
   577   done
   578 
   579 
   580 lemma rev_cut_eq:
   581   assumes "p:a=b"
   582     and "!!x. x:a=b ==> f(x):R"
   583   shows "?p:R"
   584   apply (rule assms)+
   585   done
   586 
   587 lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
   588 
   589 use "hypsubst.ML"
   590 
   591 ML {*
   592 
   593 (*** Applying HypsubstFun to generate hyp_subst_tac ***)
   594 
   595 structure Hypsubst_Data =
   596 struct
   597   (*Take apart an equality judgement; otherwise raise Match!*)
   598   fun dest_eq (Const (@{const_name Proof}, _) $
   599     (Const (@{const_name "op ="}, _)  $ t $ u) $ _) = (t, u);
   600 
   601   val imp_intr = @{thm impI}
   602 
   603   (*etac rev_cut_eq moves an equality to be the last premise. *)
   604   val rev_cut_eq = @{thm rev_cut_eq}
   605 
   606   val rev_mp = @{thm rev_mp}
   607   val subst = @{thm subst}
   608   val sym = @{thm sym}
   609   val thin_refl = @{thm thin_refl}
   610 end;
   611 
   612 structure Hypsubst = HypsubstFun(Hypsubst_Data);
   613 open Hypsubst;
   614 *}
   615 
   616 use "intprover.ML"
   617 
   618 
   619 (*** Rewrite rules ***)
   620 
   621 lemma conj_rews:
   622   "?p1 : P & True <-> P"
   623   "?p2 : True & P <-> P"
   624   "?p3 : P & False <-> False"
   625   "?p4 : False & P <-> False"
   626   "?p5 : P & P <-> P"
   627   "?p6 : P & ~P <-> False"
   628   "?p7 : ~P & P <-> False"
   629   "?p8 : (P & Q) & R <-> P & (Q & R)"
   630   apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
   631   done
   632 
   633 lemma disj_rews:
   634   "?p1 : P | True <-> True"
   635   "?p2 : True | P <-> True"
   636   "?p3 : P | False <-> P"
   637   "?p4 : False | P <-> P"
   638   "?p5 : P | P <-> P"
   639   "?p6 : (P | Q) | R <-> P | (Q | R)"
   640   apply (tactic {* IntPr.fast_tac 1 *})+
   641   done
   642 
   643 lemma not_rews:
   644   "?p1 : ~ False <-> True"
   645   "?p2 : ~ True <-> False"
   646   apply (tactic {* IntPr.fast_tac 1 *})+
   647   done
   648 
   649 lemma imp_rews:
   650   "?p1 : (P --> False) <-> ~P"
   651   "?p2 : (P --> True) <-> True"
   652   "?p3 : (False --> P) <-> True"
   653   "?p4 : (True --> P) <-> P"
   654   "?p5 : (P --> P) <-> True"
   655   "?p6 : (P --> ~P) <-> ~P"
   656   apply (tactic {* IntPr.fast_tac 1 *})+
   657   done
   658 
   659 lemma iff_rews:
   660   "?p1 : (True <-> P) <-> P"
   661   "?p2 : (P <-> True) <-> P"
   662   "?p3 : (P <-> P) <-> True"
   663   "?p4 : (False <-> P) <-> ~P"
   664   "?p5 : (P <-> False) <-> ~P"
   665   apply (tactic {* IntPr.fast_tac 1 *})+
   666   done
   667 
   668 lemma quant_rews:
   669   "?p1 : (ALL x. P) <-> P"
   670   "?p2 : (EX x. P) <-> P"
   671   apply (tactic {* IntPr.fast_tac 1 *})+
   672   done
   673 
   674 (*These are NOT supplied by default!*)
   675 lemma distrib_rews1:
   676   "?p1 : ~(P|Q) <-> ~P & ~Q"
   677   "?p2 : P & (Q | R) <-> P&Q | P&R"
   678   "?p3 : (Q | R) & P <-> Q&P | R&P"
   679   "?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)"
   680   apply (tactic {* IntPr.fast_tac 1 *})+
   681   done
   682 
   683 lemma distrib_rews2:
   684   "?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
   685   "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
   686   "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
   687   "?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"
   688   apply (tactic {* IntPr.fast_tac 1 *})+
   689   done
   690 
   691 lemmas distrib_rews = distrib_rews1 distrib_rews2
   692 
   693 lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
   694   apply (tactic {* IntPr.fast_tac 1 *})
   695   done
   696 
   697 lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
   698   apply (tactic {* IntPr.fast_tac 1 *})
   699   done
   700 
   701 end