src/FOLP/IFOLP.thy
changeset 1477 4c51ab632cda
parent 1149 5750eba8820d
child 2714 b0fbdfbbad66
     1.1 --- a/src/FOLP/IFOLP.thy	Mon Feb 05 21:29:06 1996 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Mon Feb 05 21:33:14 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	FOLP/IFOLP.thy
     1.5 +(*  Title:      FOLP/IFOLP.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Martin D Coen, Cambridge University Computer Laboratory
     1.8 +    Author:     Martin D Coen, Cambridge University Computer Laboratory
     1.9      Copyright   1992  University of Cambridge
    1.10  
    1.11  Intuitionistic First-Order Logic with Proofs
    1.12 @@ -19,41 +19,41 @@
    1.13  arities
    1.14    p,o :: logic
    1.15  
    1.16 -consts	
    1.17 +consts  
    1.18        (*** Judgements ***)
    1.19 - "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [51,10] 5)
    1.20 - Proof  	::   "[o,p]=>prop"
    1.21 + "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
    1.22 + Proof          ::   "[o,p]=>prop"
    1.23   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    1.24          
    1.25        (*** Logical Connectives -- Type Formers ***)
    1.26 - "="		::	"['a,'a] => o"	(infixl 50)
    1.27 - True,False	::	"o"
    1.28 - "Not"		::	"o => o"	("~ _" [40] 40)
    1.29 - "&"		::	"[o,o] => o"	(infixr 35)
    1.30 - "|"		::	"[o,o] => o"	(infixr 30)
    1.31 - "-->"		::	"[o,o] => o"	(infixr 25)
    1.32 - "<->"		::	"[o,o] => o"	(infixr 25)
    1.33 + "="            ::      "['a,'a] => o"  (infixl 50)
    1.34 + True,False     ::      "o"
    1.35 + "Not"          ::      "o => o"        ("~ _" [40] 40)
    1.36 + "&"            ::      "[o,o] => o"    (infixr 35)
    1.37 + "|"            ::      "[o,o] => o"    (infixr 30)
    1.38 + "-->"          ::      "[o,o] => o"    (infixr 25)
    1.39 + "<->"          ::      "[o,o] => o"    (infixr 25)
    1.40        (*Quantifiers*)
    1.41 - All		::	"('a => o) => o"	(binder "ALL " 10)
    1.42 - Ex		::	"('a => o) => o"	(binder "EX " 10)
    1.43 - Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    1.44 + All            ::      "('a => o) => o"        (binder "ALL " 10)
    1.45 + Ex             ::      "('a => o) => o"        (binder "EX " 10)
    1.46 + Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
    1.47        (*Rewriting gadgets*)
    1.48 - NORM		::	"o => o"
    1.49 - norm		::	"'a => 'a"
    1.50 + NORM           ::      "o => o"
    1.51 + norm           ::      "'a => 'a"
    1.52  
    1.53        (*** Proof Term Formers: precedence must exceed 50 ***)
    1.54 - tt		:: "p"
    1.55 - contr		:: "p=>p"
    1.56 - fst,snd	:: "p=>p"
    1.57 - pair		:: "[p,p]=>p"		("(1<_,/_>)")
    1.58 - split		:: "[p, [p,p]=>p] =>p"
    1.59 - inl,inr	:: "p=>p"
    1.60 - when		:: "[p, p=>p, p=>p]=>p"
    1.61 - lambda		:: "(p => p) => p"	(binder "lam " 55)
    1.62 - "`"		:: "[p,p]=>p"		(infixl 60)
    1.63 + tt             :: "p"
    1.64 + contr          :: "p=>p"
    1.65 + fst,snd        :: "p=>p"
    1.66 + pair           :: "[p,p]=>p"           ("(1<_,/_>)")
    1.67 + split          :: "[p, [p,p]=>p] =>p"
    1.68 + inl,inr        :: "p=>p"
    1.69 + when           :: "[p, p=>p, p=>p]=>p"
    1.70 + lambda         :: "(p => p) => p"      (binder "lam " 55)
    1.71 + "`"            :: "[p,p]=>p"           (infixl 60)
    1.72   alll           :: "['a=>p]=>p"         (binder "all " 55)
    1.73   "^"            :: "[p,'a]=>p"          (infixl 55)
    1.74 - exists		:: "['a,p]=>p"		("(1[_,/_])")
    1.75 + exists         :: "['a,p]=>p"          ("(1[_,/_])")
    1.76   xsplit         :: "[p,['a,p]=>p]=>p"
    1.77   ideq           :: "'a=>p"
    1.78   idpeel         :: "[p,'a=>p]=>p"
    1.79 @@ -66,7 +66,7 @@
    1.80  (*Equality*)
    1.81  (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
    1.82  
    1.83 -ieqI	  "ideq(a) : a=a"
    1.84 +ieqI      "ideq(a) : a=a"
    1.85  ieqE      "[| p : a=b;  !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    1.86  
    1.87  (* Truth and Falsity *)
    1.88 @@ -94,11 +94,11 @@
    1.89  
    1.90  (*Quantifiers*)
    1.91  
    1.92 -allI	  "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
    1.93 -spec	  "(f:ALL x.P(x)) ==> f^x : P(x)"
    1.94 +allI      "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
    1.95 +spec      "(f:ALL x.P(x)) ==> f^x : P(x)"
    1.96  
    1.97 -exI	  "p : P(x) ==> [x,p] : EX x.P(x)"
    1.98 -exE	  "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
    1.99 +exI       "p : P(x) ==> [x,p] : EX x.P(x)"
   1.100 +exE       "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
   1.101  
   1.102  (**** Equality between proofs ****)
   1.103  
   1.104 @@ -124,15 +124,15 @@
   1.105  
   1.106  (**** Definitions ****)
   1.107  
   1.108 -not_def 	     "~P == P-->False"
   1.109 +not_def              "~P == P-->False"
   1.110  iff_def         "P<->Q == (P-->Q) & (Q-->P)"
   1.111  
   1.112  (*Unique existence*)
   1.113  ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   1.114  
   1.115  (*Rewriting -- special constants to flag normalized terms and formulae*)
   1.116 -norm_eq	"nrm : norm(x) = x"
   1.117 -NORM_iff	"NRM : NORM(P) <-> P"
   1.118 +norm_eq "nrm : norm(x) = x"
   1.119 +NORM_iff        "NRM : NORM(P) <-> P"
   1.120  
   1.121  end
   1.122