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