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