src/FOLP/IFOLP.thy
author clasohm
Wed, 21 Jun 1995 15:01:07 +0200
changeset 1149 5750eba8820d
parent 1142 eb0e2ff8f032
child 1477 4c51ab632cda
permissions -rw-r--r--
removed \...\ inside strings
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1142
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     1
(*  Title: 	FOLP/IFOLP.thy
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     2
    ID:         $Id$
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     3
    Author: 	Martin D Coen, Cambridge University Computer Laboratory
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
Intuitionistic First-Order Logic with Proofs
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     7
*)
eb0e2ff8f032 Corrected comments in headers
lcp
parents: 648
diff changeset
     8
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
IFOLP = Pure +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
classes term < logic
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
default term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
283
76caebd18756 new type declaration syntax instead of numbers
lcp
parents: 0
diff changeset
    15
types
76caebd18756 new type declaration syntax instead of numbers
lcp
parents: 0
diff changeset
    16
  p
76caebd18756 new type declaration syntax instead of numbers
lcp
parents: 0
diff changeset
    17
  o
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
283
76caebd18756 new type declaration syntax instead of numbers
lcp
parents: 0
diff changeset
    19
arities
76caebd18756 new type declaration syntax instead of numbers
lcp
parents: 0
diff changeset
    20
  p,o :: logic
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
consts	
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
      (*** Judgements ***)
648
e27c9ec2b48b FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents: 283
diff changeset
    24
 "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [51,10] 5)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
 Proof  	::   "[o,p]=>prop"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
 EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
        
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
      (*** Logical Connectives -- Type Formers ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
 "="		::	"['a,'a] => o"	(infixl 50)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
 True,False	::	"o"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
 "Not"		::	"o => o"	("~ _" [40] 40)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
 "&"		::	"[o,o] => o"	(infixr 35)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
 "|"		::	"[o,o] => o"	(infixr 30)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
 "-->"		::	"[o,o] => o"	(infixr 25)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
 "<->"		::	"[o,o] => o"	(infixr 25)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
      (*Quantifiers*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
 All		::	"('a => o) => o"	(binder "ALL " 10)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
 Ex		::	"('a => o) => o"	(binder "EX " 10)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
 Ex1		::	"('a => o) => o"	(binder "EX! " 10)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
      (*Rewriting gadgets*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
 NORM		::	"o => o"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
 norm		::	"'a => 'a"
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 ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
 tt		:: "p"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
 contr		:: "p=>p"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
 fst,snd	:: "p=>p"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
 pair		:: "[p,p]=>p"		("(1<_,/_>)")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
 split		:: "[p, [p,p]=>p] =>p"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
 inl,inr	:: "p=>p"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
 when		:: "[p, p=>p, p=>p]=>p"
648
e27c9ec2b48b FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents: 283
diff changeset
    52
 lambda		:: "(p => p) => p"	(binder "lam " 55)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
 "`"		:: "[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)
e27c9ec2b48b FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents: 283
diff changeset
    55
 "^"            :: "[p,'a]=>p"          (infixl 55)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
 exists		:: "['a,p]=>p"		("(1[_,/_])")
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"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
 nrm, NRM       :: "p"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
(**** Propositional logic ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
(*Equality*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
(* Like Intensional Equality in MLTT - but proofs distinct from terms *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
ieqI	  "ideq(a) : a=a"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
ieqE      "[| p : a=b;  !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
(* Truth and Falsity *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
TrueI     "tt : True"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
FalseE    "a:False ==> contr(a):P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
(* Conjunction *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
conjI     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
conjunct1 "p:P&Q ==> fst(p):P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
conjunct2 "p:P&Q ==> snd(p):Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
(* Disjunction *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
disjI1    "a:P ==> inl(a):P|Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
disjI2    "b:Q ==> inr(b):P|Q"
1149
5750eba8820d removed \...\ inside strings
clasohm
parents: 1142
diff changeset
    87
disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R 
5750eba8820d removed \...\ inside strings
clasohm
parents: 1142
diff changeset
    88
          |] ==> when(a,f,g):R"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
(* Implication *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
impI      "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P-->Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
(*Quantifiers*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
allI	  "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
spec	  "(f:ALL x.P(x)) ==> f^x : P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
exI	  "p : P(x) ==> [x,p] : EX x.P(x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
exE	  "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
(**** Equality between proofs ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
prefl     "a : P ==> a = a : P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
psym      "a = b : P ==> b = a : P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
idpeelB   "[| !!x.f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
fstB      "a:P ==> fst(<a,b>) = a : P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
sndB      "b:Q ==> snd(<a,b>) = b : Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
whenBinl  "[| a:P;  !!x.x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
whenBinr  "[| b:P;  !!x.x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
plusEC    "a:P|Q ==> when(a,%x.inl(x),%y.inr(y)) = p : P|Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
applyB     "[| a:P;  !!x.x:P ==> b(x) : Q |] ==> (lam x.b(x)) ` a = b(a) : Q"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
funEC      "f:P ==> f = lam x.f`x : P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
specB      "[| !!x.f(x) : P(x) |] ==> (all x.f(x)) ^ a = f(a) : P(a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
(**** Definitions ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
not_def 	     "~P == P-->False"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
iff_def         "P<->Q == (P-->Q) & (Q-->P)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
(*Unique existence*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
(*Rewriting -- special constants to flag normalized terms and formulae*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
norm_eq	"nrm : norm(x) = x"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
NORM_iff	"NRM : NORM(P) <-> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val show_proofs = ref false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
fun proof_tr' [P,p] = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
    if !show_proofs then Const("@Proof",dummyT) $ p $ P 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
    else P  (*this case discards the proof term*);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val  parse_translation = [("@Proof", proof_tr)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
val print_translation  = [("Proof", proof_tr')];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152