expanded tabs
authorclasohm
Mon Feb 05 21:33:14 1996 +0100 (1996-02-05)
changeset 14774c51ab632cda
parent 1476 608483c2122a
child 1478 2b8c2a7547ab
expanded tabs
src/FOLP/FOLP.thy
src/FOLP/IFOLP.thy
src/FOLP/ex/Nat.thy
src/FOLP/ex/Prolog.thy
     1.1 --- a/src/FOLP/FOLP.thy	Mon Feb 05 21:29:06 1996 +0100
     1.2 +++ b/src/FOLP/FOLP.thy	Mon Feb 05 21:33:14 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	FOLP/FOLP.thy
     1.5 +(*  Title:      FOLP/FOLP.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  Classical First-Order Logic with Proofs
     2.1 --- a/src/FOLP/IFOLP.thy	Mon Feb 05 21:29:06 1996 +0100
     2.2 +++ b/src/FOLP/IFOLP.thy	Mon Feb 05 21:33:14 1996 +0100
     2.3 @@ -1,6 +1,6 @@
     2.4 -(*  Title: 	FOLP/IFOLP.thy
     2.5 +(*  Title:      FOLP/IFOLP.thy
     2.6      ID:         $Id$
     2.7 -    Author: 	Martin D Coen, Cambridge University Computer Laboratory
     2.8 +    Author:     Martin D Coen, Cambridge University Computer Laboratory
     2.9      Copyright   1992  University of Cambridge
    2.10  
    2.11  Intuitionistic First-Order Logic with Proofs
    2.12 @@ -19,41 +19,41 @@
    2.13  arities
    2.14    p,o :: logic
    2.15  
    2.16 -consts	
    2.17 +consts  
    2.18        (*** Judgements ***)
    2.19 - "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [51,10] 5)
    2.20 - Proof  	::   "[o,p]=>prop"
    2.21 + "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
    2.22 + Proof          ::   "[o,p]=>prop"
    2.23   EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    2.24          
    2.25        (*** Logical Connectives -- Type Formers ***)
    2.26 - "="		::	"['a,'a] => o"	(infixl 50)
    2.27 - True,False	::	"o"
    2.28 - "Not"		::	"o => o"	("~ _" [40] 40)
    2.29 - "&"		::	"[o,o] => o"	(infixr 35)
    2.30 - "|"		::	"[o,o] => o"	(infixr 30)
    2.31 - "-->"		::	"[o,o] => o"	(infixr 25)
    2.32 - "<->"		::	"[o,o] => o"	(infixr 25)
    2.33 + "="            ::      "['a,'a] => o"  (infixl 50)
    2.34 + True,False     ::      "o"
    2.35 + "Not"          ::      "o => o"        ("~ _" [40] 40)
    2.36 + "&"            ::      "[o,o] => o"    (infixr 35)
    2.37 + "|"            ::      "[o,o] => o"    (infixr 30)
    2.38 + "-->"          ::      "[o,o] => o"    (infixr 25)
    2.39 + "<->"          ::      "[o,o] => o"    (infixr 25)
    2.40        (*Quantifiers*)
    2.41 - All		::	"('a => o) => o"	(binder "ALL " 10)
    2.42 - Ex		::	"('a => o) => o"	(binder "EX " 10)
    2.43 - Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    2.44 + All            ::      "('a => o) => o"        (binder "ALL " 10)
    2.45 + Ex             ::      "('a => o) => o"        (binder "EX " 10)
    2.46 + Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
    2.47        (*Rewriting gadgets*)
    2.48 - NORM		::	"o => o"
    2.49 - norm		::	"'a => 'a"
    2.50 + NORM           ::      "o => o"
    2.51 + norm           ::      "'a => 'a"
    2.52  
    2.53        (*** Proof Term Formers: precedence must exceed 50 ***)
    2.54 - tt		:: "p"
    2.55 - contr		:: "p=>p"
    2.56 - fst,snd	:: "p=>p"
    2.57 - pair		:: "[p,p]=>p"		("(1<_,/_>)")
    2.58 - split		:: "[p, [p,p]=>p] =>p"
    2.59 - inl,inr	:: "p=>p"
    2.60 - when		:: "[p, p=>p, p=>p]=>p"
    2.61 - lambda		:: "(p => p) => p"	(binder "lam " 55)
    2.62 - "`"		:: "[p,p]=>p"		(infixl 60)
    2.63 + tt             :: "p"
    2.64 + contr          :: "p=>p"
    2.65 + fst,snd        :: "p=>p"
    2.66 + pair           :: "[p,p]=>p"           ("(1<_,/_>)")
    2.67 + split          :: "[p, [p,p]=>p] =>p"
    2.68 + inl,inr        :: "p=>p"
    2.69 + when           :: "[p, p=>p, p=>p]=>p"
    2.70 + lambda         :: "(p => p) => p"      (binder "lam " 55)
    2.71 + "`"            :: "[p,p]=>p"           (infixl 60)
    2.72   alll           :: "['a=>p]=>p"         (binder "all " 55)
    2.73   "^"            :: "[p,'a]=>p"          (infixl 55)
    2.74 - exists		:: "['a,p]=>p"		("(1[_,/_])")
    2.75 + exists         :: "['a,p]=>p"          ("(1[_,/_])")
    2.76   xsplit         :: "[p,['a,p]=>p]=>p"
    2.77   ideq           :: "'a=>p"
    2.78   idpeel         :: "[p,'a=>p]=>p"
    2.79 @@ -66,7 +66,7 @@
    2.80  (*Equality*)
    2.81  (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
    2.82  
    2.83 -ieqI	  "ideq(a) : a=a"
    2.84 +ieqI      "ideq(a) : a=a"
    2.85  ieqE      "[| p : a=b;  !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    2.86  
    2.87  (* Truth and Falsity *)
    2.88 @@ -94,11 +94,11 @@
    2.89  
    2.90  (*Quantifiers*)
    2.91  
    2.92 -allI	  "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
    2.93 -spec	  "(f:ALL x.P(x)) ==> f^x : P(x)"
    2.94 +allI      "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
    2.95 +spec      "(f:ALL x.P(x)) ==> f^x : P(x)"
    2.96  
    2.97 -exI	  "p : P(x) ==> [x,p] : EX x.P(x)"
    2.98 -exE	  "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
    2.99 +exI       "p : P(x) ==> [x,p] : EX x.P(x)"
   2.100 +exE       "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
   2.101  
   2.102  (**** Equality between proofs ****)
   2.103  
   2.104 @@ -124,15 +124,15 @@
   2.105  
   2.106  (**** Definitions ****)
   2.107  
   2.108 -not_def 	     "~P == P-->False"
   2.109 +not_def              "~P == P-->False"
   2.110  iff_def         "P<->Q == (P-->Q) & (Q-->P)"
   2.111  
   2.112  (*Unique existence*)
   2.113  ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   2.114  
   2.115  (*Rewriting -- special constants to flag normalized terms and formulae*)
   2.116 -norm_eq	"nrm : norm(x) = x"
   2.117 -NORM_iff	"NRM : NORM(P) <-> P"
   2.118 +norm_eq "nrm : norm(x) = x"
   2.119 +NORM_iff        "NRM : NORM(P) <-> P"
   2.120  
   2.121  end
   2.122  
     3.1 --- a/src/FOLP/ex/Nat.thy	Mon Feb 05 21:29:06 1996 +0100
     3.2 +++ b/src/FOLP/ex/Nat.thy	Mon Feb 05 21:33:14 1996 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4 -(*  Title: 	FOLP/ex/nat.thy
     3.5 +(*  Title:      FOLP/ex/nat.thy
     3.6      ID:         $Id$
     3.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     3.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.9      Copyright   1992  University of Cambridge
    3.10  
    3.11  Examples for the manual "Introduction to Isabelle"
     4.1 --- a/src/FOLP/ex/Prolog.thy	Mon Feb 05 21:29:06 1996 +0100
     4.2 +++ b/src/FOLP/ex/Prolog.thy	Mon Feb 05 21:33:14 1996 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4 -(*  Title: 	FOLP/ex/Prolog.thy
     4.5 +(*  Title:      FOLP/ex/Prolog.thy
     4.6      ID:         $Id$
     4.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.9      Copyright   1992  University of Cambridge
    4.10  
    4.11  First-Order Logic: PROLOG examples