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