added white-space;
authorwenzelm
Mon Oct 25 12:32:53 1993 +0100 (1993-10-25)
changeset 7974e68ed3b4fd
parent 78 e76a1edc2e49
child 80 0d10b8a501d5
added white-space;
made ~= a fake infix;
src/FOL/IFOL.thy
src/FOL/ifol.thy
     1.1 --- a/src/FOL/IFOL.thy	Fri Oct 22 22:17:25 1993 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Mon Oct 25 12:32:53 1993 +0100
     1.3 @@ -1,83 +1,97 @@
     1.4 -(*  Title: 	FOL/ifol.thy
     1.5 +(*  Title:      FOL/ifol.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1993  University of Cambridge
    1.10  
    1.11  Intuitionistic first-order logic
    1.12  *)
    1.13  
    1.14 -IFOL = Pure + 
    1.15 +IFOL = Pure +
    1.16  
    1.17 -classes term < logic
    1.18 +classes
    1.19 +  term < logic
    1.20 +
    1.21 +default
    1.22 +  term
    1.23  
    1.24 -default term
    1.25 +types
    1.26 +  o 0
    1.27  
    1.28 -types o 0
    1.29 +arities
    1.30 +  o :: logic
    1.31  
    1.32 -arities o :: logic
    1.33 +
    1.34 +consts
    1.35  
    1.36 -consts	
    1.37 -    Trueprop	::	"o => prop"		("(_)" [0] 5)
    1.38 -    True, False	::	"o"
    1.39 -  (*Connectives*)
    1.40 -    "=", "~="	::	"['a,'a] => o"		(infixl 50)
    1.41 +  Trueprop      :: "o => prop"                  ("(_)" 5)
    1.42 +  True, False   :: "o"
    1.43 +
    1.44 +  (* Connectives *)
    1.45 +
    1.46 +  "="           :: "['a, 'a] => o"              (infixl 50)
    1.47 +  "~="          :: "['a, 'a] => o"              ("(_ ~=/ _)" [50, 51] 50)
    1.48  
    1.49 -    Not		::	"o => o"		("~ _" [40] 40)
    1.50 -    "&"		::	"[o,o] => o"		(infixr 35)
    1.51 -    "|"		::	"[o,o] => o"		(infixr 30)
    1.52 -    "-->"	::	"[o,o] => o"		(infixr 25)
    1.53 -    "<->"	::	"[o,o] => o"		(infixr 25)
    1.54 -  
    1.55 -  (*Quantifiers*)
    1.56 -    All		::	"('a => o) => o"	(binder "ALL " 10)
    1.57 -    Ex		::	"('a => o) => o"	(binder "EX " 10)
    1.58 -    Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    1.59 +  Not           :: "o => o"                     ("~ _" [40] 40)
    1.60 +  "&"           :: "[o, o] => o"                (infixr 35)
    1.61 +  "|"           :: "[o, o] => o"                (infixr 30)
    1.62 +  "-->"         :: "[o, o] => o"                (infixr 25)
    1.63 +  "<->"         :: "[o, o] => o"                (infixr 25)
    1.64 +
    1.65 +  (* Quantifiers *)
    1.66 +
    1.67 +  All           :: "('a => o) => o"             (binder "ALL " 10)
    1.68 +  Ex            :: "('a => o) => o"             (binder "EX " 10)
    1.69 +  Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    1.70 +
    1.71  
    1.72  translations
    1.73 -    "x ~= y"    == "~ (x=y)"
    1.74 +  "x ~= y"      == "~ (x = y)"
    1.75 +
    1.76  
    1.77  rules
    1.78  
    1.79 -  (*Equality*)
    1.80 +  (* Equality *)
    1.81  
    1.82 -refl		"a=a"
    1.83 -subst		"[| a=b;  P(a) |] ==> P(b)"
    1.84 +  refl          "a=a"
    1.85 +  subst         "[| a=b;  P(a) |] ==> P(b)"
    1.86  
    1.87 -  (*Propositional logic*)
    1.88 +  (* Propositional logic *)
    1.89  
    1.90 -conjI		"[| P;  Q |] ==> P&Q"
    1.91 -conjunct1	"P&Q ==> P"
    1.92 -conjunct2	"P&Q ==> Q"
    1.93 +  conjI         "[| P;  Q |] ==> P&Q"
    1.94 +  conjunct1     "P&Q ==> P"
    1.95 +  conjunct2     "P&Q ==> Q"
    1.96  
    1.97 -disjI1		"P ==> P|Q"
    1.98 -disjI2		"Q ==> P|Q"
    1.99 -disjE		"[| P|Q;  P ==> R;  Q ==> R |] ==> R"
   1.100 +  disjI1        "P ==> P|Q"
   1.101 +  disjI2        "Q ==> P|Q"
   1.102 +  disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
   1.103  
   1.104 -impI		"(P ==> Q) ==> P-->Q"
   1.105 -mp		"[| P-->Q;  P |] ==> Q"
   1.106 +  impI          "(P ==> Q) ==> P-->Q"
   1.107 +  mp            "[| P-->Q;  P |] ==> Q"
   1.108  
   1.109 -FalseE		"False ==> P"
   1.110 +  FalseE        "False ==> P"
   1.111  
   1.112 -  (*Definitions*)
   1.113 +  (* Definitions *)
   1.114  
   1.115 -True_def	"True  == False-->False"
   1.116 -not_def		"~P    == P-->False"
   1.117 -iff_def		"P<->Q == (P-->Q) & (Q-->P)"
   1.118 +  True_def      "True  == False-->False"
   1.119 +  not_def       "~P    == P-->False"
   1.120 +  iff_def       "P<->Q == (P-->Q) & (Q-->P)"
   1.121 +
   1.122 +  (* Unique existence *)
   1.123  
   1.124 -  (*Unique existence*)
   1.125 -ex1_def		"EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   1.126 +  ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   1.127  
   1.128 -  (*Quantifiers*)
   1.129 +  (* Quantifiers *)
   1.130  
   1.131 -allI		"(!!x. P(x)) ==> (ALL x.P(x))"
   1.132 -spec		"(ALL x.P(x)) ==> P(x)"
   1.133 +  allI          "(!!x. P(x)) ==> (ALL x.P(x))"
   1.134 +  spec          "(ALL x.P(x)) ==> P(x)"
   1.135  
   1.136 -exI		"P(x) ==> (EX x.P(x))"
   1.137 -exE		"[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
   1.138 +  exI           "P(x) ==> (EX x.P(x))"
   1.139 +  exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
   1.140  
   1.141    (* Reflection *)
   1.142  
   1.143 -eq_reflection  "(x=y)   ==> (x==y)"
   1.144 -iff_reflection "(P<->Q) ==> (P==Q)"
   1.145 +  eq_reflection   "(x=y)   ==> (x==y)"
   1.146 +  iff_reflection  "(P<->Q) ==> (P==Q)"
   1.147  
   1.148  end
   1.149 +
     2.1 --- a/src/FOL/ifol.thy	Fri Oct 22 22:17:25 1993 +0100
     2.2 +++ b/src/FOL/ifol.thy	Mon Oct 25 12:32:53 1993 +0100
     2.3 @@ -1,83 +1,97 @@
     2.4 -(*  Title: 	FOL/ifol.thy
     2.5 +(*  Title:      FOL/ifol.thy
     2.6      ID:         $Id$
     2.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.9      Copyright   1993  University of Cambridge
    2.10  
    2.11  Intuitionistic first-order logic
    2.12  *)
    2.13  
    2.14 -IFOL = Pure + 
    2.15 +IFOL = Pure +
    2.16  
    2.17 -classes term < logic
    2.18 +classes
    2.19 +  term < logic
    2.20 +
    2.21 +default
    2.22 +  term
    2.23  
    2.24 -default term
    2.25 +types
    2.26 +  o 0
    2.27  
    2.28 -types o 0
    2.29 +arities
    2.30 +  o :: logic
    2.31  
    2.32 -arities o :: logic
    2.33 +
    2.34 +consts
    2.35  
    2.36 -consts	
    2.37 -    Trueprop	::	"o => prop"		("(_)" [0] 5)
    2.38 -    True, False	::	"o"
    2.39 -  (*Connectives*)
    2.40 -    "=", "~="	::	"['a,'a] => o"		(infixl 50)
    2.41 +  Trueprop      :: "o => prop"                  ("(_)" 5)
    2.42 +  True, False   :: "o"
    2.43 +
    2.44 +  (* Connectives *)
    2.45 +
    2.46 +  "="           :: "['a, 'a] => o"              (infixl 50)
    2.47 +  "~="          :: "['a, 'a] => o"              ("(_ ~=/ _)" [50, 51] 50)
    2.48  
    2.49 -    Not		::	"o => o"		("~ _" [40] 40)
    2.50 -    "&"		::	"[o,o] => o"		(infixr 35)
    2.51 -    "|"		::	"[o,o] => o"		(infixr 30)
    2.52 -    "-->"	::	"[o,o] => o"		(infixr 25)
    2.53 -    "<->"	::	"[o,o] => o"		(infixr 25)
    2.54 -  
    2.55 -  (*Quantifiers*)
    2.56 -    All		::	"('a => o) => o"	(binder "ALL " 10)
    2.57 -    Ex		::	"('a => o) => o"	(binder "EX " 10)
    2.58 -    Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    2.59 +  Not           :: "o => o"                     ("~ _" [40] 40)
    2.60 +  "&"           :: "[o, o] => o"                (infixr 35)
    2.61 +  "|"           :: "[o, o] => o"                (infixr 30)
    2.62 +  "-->"         :: "[o, o] => o"                (infixr 25)
    2.63 +  "<->"         :: "[o, o] => o"                (infixr 25)
    2.64 +
    2.65 +  (* Quantifiers *)
    2.66 +
    2.67 +  All           :: "('a => o) => o"             (binder "ALL " 10)
    2.68 +  Ex            :: "('a => o) => o"             (binder "EX " 10)
    2.69 +  Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    2.70 +
    2.71  
    2.72  translations
    2.73 -    "x ~= y"    == "~ (x=y)"
    2.74 +  "x ~= y"      == "~ (x = y)"
    2.75 +
    2.76  
    2.77  rules
    2.78  
    2.79 -  (*Equality*)
    2.80 +  (* Equality *)
    2.81  
    2.82 -refl		"a=a"
    2.83 -subst		"[| a=b;  P(a) |] ==> P(b)"
    2.84 +  refl          "a=a"
    2.85 +  subst         "[| a=b;  P(a) |] ==> P(b)"
    2.86  
    2.87 -  (*Propositional logic*)
    2.88 +  (* Propositional logic *)
    2.89  
    2.90 -conjI		"[| P;  Q |] ==> P&Q"
    2.91 -conjunct1	"P&Q ==> P"
    2.92 -conjunct2	"P&Q ==> Q"
    2.93 +  conjI         "[| P;  Q |] ==> P&Q"
    2.94 +  conjunct1     "P&Q ==> P"
    2.95 +  conjunct2     "P&Q ==> Q"
    2.96  
    2.97 -disjI1		"P ==> P|Q"
    2.98 -disjI2		"Q ==> P|Q"
    2.99 -disjE		"[| P|Q;  P ==> R;  Q ==> R |] ==> R"
   2.100 +  disjI1        "P ==> P|Q"
   2.101 +  disjI2        "Q ==> P|Q"
   2.102 +  disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
   2.103  
   2.104 -impI		"(P ==> Q) ==> P-->Q"
   2.105 -mp		"[| P-->Q;  P |] ==> Q"
   2.106 +  impI          "(P ==> Q) ==> P-->Q"
   2.107 +  mp            "[| P-->Q;  P |] ==> Q"
   2.108  
   2.109 -FalseE		"False ==> P"
   2.110 +  FalseE        "False ==> P"
   2.111  
   2.112 -  (*Definitions*)
   2.113 +  (* Definitions *)
   2.114  
   2.115 -True_def	"True  == False-->False"
   2.116 -not_def		"~P    == P-->False"
   2.117 -iff_def		"P<->Q == (P-->Q) & (Q-->P)"
   2.118 +  True_def      "True  == False-->False"
   2.119 +  not_def       "~P    == P-->False"
   2.120 +  iff_def       "P<->Q == (P-->Q) & (Q-->P)"
   2.121 +
   2.122 +  (* Unique existence *)
   2.123  
   2.124 -  (*Unique existence*)
   2.125 -ex1_def		"EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   2.126 +  ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   2.127  
   2.128 -  (*Quantifiers*)
   2.129 +  (* Quantifiers *)
   2.130  
   2.131 -allI		"(!!x. P(x)) ==> (ALL x.P(x))"
   2.132 -spec		"(ALL x.P(x)) ==> P(x)"
   2.133 +  allI          "(!!x. P(x)) ==> (ALL x.P(x))"
   2.134 +  spec          "(ALL x.P(x)) ==> P(x)"
   2.135  
   2.136 -exI		"P(x) ==> (EX x.P(x))"
   2.137 -exE		"[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
   2.138 +  exI           "P(x) ==> (EX x.P(x))"
   2.139 +  exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
   2.140  
   2.141    (* Reflection *)
   2.142  
   2.143 -eq_reflection  "(x=y)   ==> (x==y)"
   2.144 -iff_reflection "(P<->Q) ==> (P==Q)"
   2.145 +  eq_reflection   "(x=y)   ==> (x==y)"
   2.146 +  iff_reflection  "(P<->Q) ==> (P==Q)"
   2.147  
   2.148  end
   2.149 +