src/FOLP/IFOLP.thy
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 17480 fd19f77dcf60
child 26322 eaf634e975fa
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
     1
(*  Title:      FOLP/IFOLP.thy
1142
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     2
    ID:         $Id$
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
     3
    Author:     Martin D Coen, Cambridge University Computer Laboratory
1142
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     4
    Copyright   1992  University of Cambridge
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     5
*)
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     6
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     7
header {* Intuitionistic First-Order Logic with Proofs *}
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     8
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
     9
theory IFOLP
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    10
imports Pure
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    11
begin
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
3942
1f1c1f524d19 adapted to qualified names;
wenzelm
parents: 3836
diff changeset
    13
global
1f1c1f524d19 adapted to qualified names;
wenzelm
parents: 3836
diff changeset
    14
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    15
classes "term"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    16
defaultsort "term"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    18
typedecl p
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    19
typedecl o
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    21
consts
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
      (*** Judgements ***)
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    23
 "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    24
 Proof          ::   "[o,p]=>prop"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
 EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    26
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
      (*** Logical Connectives -- Type Formers ***)
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    28
 "="            ::      "['a,'a] => o"  (infixl 50)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    29
 True           ::      "o"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    30
 False          ::      "o"
2714
b0fbdfbbad66 Removed needless quotes
paulson
parents: 1477
diff changeset
    31
 Not            ::      "o => o"        ("~ _" [40] 40)
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    32
 "&"            ::      "[o,o] => o"    (infixr 35)
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    33
 "|"            ::      "[o,o] => o"    (infixr 30)
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    34
 "-->"          ::      "[o,o] => o"    (infixr 25)
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    35
 "<->"          ::      "[o,o] => o"    (infixr 25)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
      (*Quantifiers*)
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    37
 All            ::      "('a => o) => o"        (binder "ALL " 10)
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    38
 Ex             ::      "('a => o) => o"        (binder "EX " 10)
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    39
 Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
      (*Rewriting gadgets*)
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    41
 NORM           ::      "o => o"
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    42
 norm           ::      "'a => 'a"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
648
e27c9ec2b48b FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents: 283
diff changeset
    44
      (*** Proof Term Formers: precedence must exceed 50 ***)
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    45
 tt             :: "p"
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    46
 contr          :: "p=>p"
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    47
 fst            :: "p=>p"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    48
 snd            :: "p=>p"
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    49
 pair           :: "[p,p]=>p"           ("(1<_,/_>)")
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    50
 split          :: "[p, [p,p]=>p] =>p"
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    51
 inl            :: "p=>p"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    52
 inr            :: "p=>p"
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    53
 when           :: "[p, p=>p, p=>p]=>p"
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    54
 lambda         :: "(p => p) => p"      (binder "lam " 55)
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    55
 "`"            :: "[p,p]=>p"           (infixl 60)
648
e27c9ec2b48b FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents: 283
diff changeset
    56
 alll           :: "['a=>p]=>p"         (binder "all " 55)
e27c9ec2b48b FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents: 283
diff changeset
    57
 "^"            :: "[p,'a]=>p"          (infixl 55)
1477
4c51ab632cda expanded tabs
clasohm
parents: 1149
diff changeset
    58
 exists         :: "['a,p]=>p"          ("(1[_,/_])")
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
 xsplit         :: "[p,['a,p]=>p]=>p"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
 ideq           :: "'a=>p"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
 idpeel         :: "[p,'a=>p]=>p"
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    62
 nrm            :: p
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    63
 NRM            :: p
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
3942
1f1c1f524d19 adapted to qualified names;
wenzelm
parents: 3836
diff changeset
    65
local
1f1c1f524d19 adapted to qualified names;
wenzelm
parents: 3836
diff changeset
    66
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    67
ML {*
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    68
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    69
(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    70
val show_proofs = ref false;
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    71
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    72
fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    73
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    74
fun proof_tr' [P,p] =
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    75
    if !show_proofs then Const("@Proof",dummyT) $ p $ P
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    76
    else P  (*this case discards the proof term*);
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    77
*}
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    78
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    79
parse_translation {* [("@Proof", proof_tr)] *}
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    80
print_translation {* [("Proof", proof_tr')] *}
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    81
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    82
axioms
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
(**** Propositional logic ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
(*Equality*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
(* Like Intensional Equality in MLTT - but proofs distinct from terms *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    89
ieqI:      "ideq(a) : a=a"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    90
ieqE:      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
(* Truth and Falsity *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    94
TrueI:     "tt : True"
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
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
    99
conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   100
conjunct1: "p:P&Q ==> fst(p):P"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   101
conjunct2: "p:P&Q ==> snd(p):Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
(* Disjunction *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   105
disjI1:    "a:P ==> inl(a):P|Q"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   106
disjI2:    "b:Q ==> inr(b):P|Q"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   107
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
   108
           |] ==> when(a,f,g):R"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
(* Implication *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   112
impI:      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   113
mp:        "[| f:P-->Q;  a:P |] ==> f`a:Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
(*Quantifiers*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   117
allI:      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   118
spec:      "(f:ALL x. P(x)) ==> f^x : P(x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   120
exI:       "p : P(x) ==> [x,p] : EX x. P(x)"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   121
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
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
(**** Equality between proofs ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   125
prefl:     "a : P ==> a = a : P"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   126
psym:      "a = b : P ==> b = a : P"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   127
ptrans:    "[| a = b : P;  b = c : P |] ==> a = c : P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   129
idpeelB:   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   131
fstB:      "a:P ==> fst(<a,b>) = a : P"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   132
sndB:      "b:Q ==> snd(<a,b>) = b : Q"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   133
pairEC:    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   135
whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   136
whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   137
plusEC:    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   139
applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   140
funEC:      "f:P ==> f = lam x. f`x : P"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   142
specB:      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
(**** Definitions ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   147
not_def:              "~P == P-->False"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   148
iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
(*Unique existence*)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   151
ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
(*Rewriting -- special constants to flag normalized terms and formulae*)
17480
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   154
norm_eq: "nrm : norm(x) = x"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   155
NORM_iff:        "NRM : NORM(P) <-> P"
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   156
fd19f77dcf60 converted to Isar theory format;
wenzelm
parents: 14854
diff changeset
   157
ML {* use_legacy_bindings (the_context ()) *}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161