--- a/src/FOL/IFOL.thy Fri Oct 22 22:17:25 1993 +0100
+++ b/src/FOL/IFOL.thy Mon Oct 25 12:32:53 1993 +0100
@@ -1,83 +1,97 @@
-(* Title: FOL/ifol.thy
+(* Title: FOL/ifol.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Intuitionistic first-order logic
*)
-IFOL = Pure +
+IFOL = Pure +
-classes term < logic
+classes
+ term < logic
+
+default
+ term
-default term
+types
+ o 0
-types o 0
+arities
+ o :: logic
-arities o :: logic
+
+consts
-consts
- Trueprop :: "o => prop" ("(_)" [0] 5)
- True, False :: "o"
- (*Connectives*)
- "=", "~=" :: "['a,'a] => o" (infixl 50)
+ Trueprop :: "o => prop" ("(_)" 5)
+ True, False :: "o"
+
+ (* Connectives *)
+
+ "=" :: "['a, 'a] => o" (infixl 50)
+ "~=" :: "['a, 'a] => o" ("(_ ~=/ _)" [50, 51] 50)
- Not :: "o => o" ("~ _" [40] 40)
- "&" :: "[o,o] => o" (infixr 35)
- "|" :: "[o,o] => o" (infixr 30)
- "-->" :: "[o,o] => o" (infixr 25)
- "<->" :: "[o,o] => o" (infixr 25)
-
- (*Quantifiers*)
- All :: "('a => o) => o" (binder "ALL " 10)
- Ex :: "('a => o) => o" (binder "EX " 10)
- Ex1 :: "('a => o) => o" (binder "EX! " 10)
+ Not :: "o => o" ("~ _" [40] 40)
+ "&" :: "[o, o] => o" (infixr 35)
+ "|" :: "[o, o] => o" (infixr 30)
+ "-->" :: "[o, o] => o" (infixr 25)
+ "<->" :: "[o, o] => o" (infixr 25)
+
+ (* Quantifiers *)
+
+ All :: "('a => o) => o" (binder "ALL " 10)
+ Ex :: "('a => o) => o" (binder "EX " 10)
+ Ex1 :: "('a => o) => o" (binder "EX! " 10)
+
translations
- "x ~= y" == "~ (x=y)"
+ "x ~= y" == "~ (x = y)"
+
rules
- (*Equality*)
+ (* Equality *)
-refl "a=a"
-subst "[| a=b; P(a) |] ==> P(b)"
+ refl "a=a"
+ subst "[| a=b; P(a) |] ==> P(b)"
- (*Propositional logic*)
+ (* Propositional logic *)
-conjI "[| P; Q |] ==> P&Q"
-conjunct1 "P&Q ==> P"
-conjunct2 "P&Q ==> Q"
+ conjI "[| P; Q |] ==> P&Q"
+ conjunct1 "P&Q ==> P"
+ conjunct2 "P&Q ==> Q"
-disjI1 "P ==> P|Q"
-disjI2 "Q ==> P|Q"
-disjE "[| P|Q; P ==> R; Q ==> R |] ==> R"
+ disjI1 "P ==> P|Q"
+ disjI2 "Q ==> P|Q"
+ disjE "[| P|Q; P ==> R; Q ==> R |] ==> R"
-impI "(P ==> Q) ==> P-->Q"
-mp "[| P-->Q; P |] ==> Q"
+ impI "(P ==> Q) ==> P-->Q"
+ mp "[| P-->Q; P |] ==> Q"
-FalseE "False ==> P"
+ FalseE "False ==> P"
- (*Definitions*)
+ (* Definitions *)
-True_def "True == False-->False"
-not_def "~P == P-->False"
-iff_def "P<->Q == (P-->Q) & (Q-->P)"
+ True_def "True == False-->False"
+ not_def "~P == P-->False"
+ iff_def "P<->Q == (P-->Q) & (Q-->P)"
+
+ (* Unique existence *)
- (*Unique existence*)
-ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+ ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
- (*Quantifiers*)
+ (* Quantifiers *)
-allI "(!!x. P(x)) ==> (ALL x.P(x))"
-spec "(ALL x.P(x)) ==> P(x)"
+ allI "(!!x. P(x)) ==> (ALL x.P(x))"
+ spec "(ALL x.P(x)) ==> P(x)"
-exI "P(x) ==> (EX x.P(x))"
-exE "[| EX x.P(x); !!x. P(x) ==> R |] ==> R"
+ exI "P(x) ==> (EX x.P(x))"
+ exE "[| EX x.P(x); !!x. P(x) ==> R |] ==> R"
(* Reflection *)
-eq_reflection "(x=y) ==> (x==y)"
-iff_reflection "(P<->Q) ==> (P==Q)"
+ eq_reflection "(x=y) ==> (x==y)"
+ iff_reflection "(P<->Q) ==> (P==Q)"
end
+
--- a/src/FOL/ifol.thy Fri Oct 22 22:17:25 1993 +0100
+++ b/src/FOL/ifol.thy Mon Oct 25 12:32:53 1993 +0100
@@ -1,83 +1,97 @@
-(* Title: FOL/ifol.thy
+(* Title: FOL/ifol.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Intuitionistic first-order logic
*)
-IFOL = Pure +
+IFOL = Pure +
-classes term < logic
+classes
+ term < logic
+
+default
+ term
-default term
+types
+ o 0
-types o 0
+arities
+ o :: logic
-arities o :: logic
+
+consts
-consts
- Trueprop :: "o => prop" ("(_)" [0] 5)
- True, False :: "o"
- (*Connectives*)
- "=", "~=" :: "['a,'a] => o" (infixl 50)
+ Trueprop :: "o => prop" ("(_)" 5)
+ True, False :: "o"
+
+ (* Connectives *)
+
+ "=" :: "['a, 'a] => o" (infixl 50)
+ "~=" :: "['a, 'a] => o" ("(_ ~=/ _)" [50, 51] 50)
- Not :: "o => o" ("~ _" [40] 40)
- "&" :: "[o,o] => o" (infixr 35)
- "|" :: "[o,o] => o" (infixr 30)
- "-->" :: "[o,o] => o" (infixr 25)
- "<->" :: "[o,o] => o" (infixr 25)
-
- (*Quantifiers*)
- All :: "('a => o) => o" (binder "ALL " 10)
- Ex :: "('a => o) => o" (binder "EX " 10)
- Ex1 :: "('a => o) => o" (binder "EX! " 10)
+ Not :: "o => o" ("~ _" [40] 40)
+ "&" :: "[o, o] => o" (infixr 35)
+ "|" :: "[o, o] => o" (infixr 30)
+ "-->" :: "[o, o] => o" (infixr 25)
+ "<->" :: "[o, o] => o" (infixr 25)
+
+ (* Quantifiers *)
+
+ All :: "('a => o) => o" (binder "ALL " 10)
+ Ex :: "('a => o) => o" (binder "EX " 10)
+ Ex1 :: "('a => o) => o" (binder "EX! " 10)
+
translations
- "x ~= y" == "~ (x=y)"
+ "x ~= y" == "~ (x = y)"
+
rules
- (*Equality*)
+ (* Equality *)
-refl "a=a"
-subst "[| a=b; P(a) |] ==> P(b)"
+ refl "a=a"
+ subst "[| a=b; P(a) |] ==> P(b)"
- (*Propositional logic*)
+ (* Propositional logic *)
-conjI "[| P; Q |] ==> P&Q"
-conjunct1 "P&Q ==> P"
-conjunct2 "P&Q ==> Q"
+ conjI "[| P; Q |] ==> P&Q"
+ conjunct1 "P&Q ==> P"
+ conjunct2 "P&Q ==> Q"
-disjI1 "P ==> P|Q"
-disjI2 "Q ==> P|Q"
-disjE "[| P|Q; P ==> R; Q ==> R |] ==> R"
+ disjI1 "P ==> P|Q"
+ disjI2 "Q ==> P|Q"
+ disjE "[| P|Q; P ==> R; Q ==> R |] ==> R"
-impI "(P ==> Q) ==> P-->Q"
-mp "[| P-->Q; P |] ==> Q"
+ impI "(P ==> Q) ==> P-->Q"
+ mp "[| P-->Q; P |] ==> Q"
-FalseE "False ==> P"
+ FalseE "False ==> P"
- (*Definitions*)
+ (* Definitions *)
-True_def "True == False-->False"
-not_def "~P == P-->False"
-iff_def "P<->Q == (P-->Q) & (Q-->P)"
+ True_def "True == False-->False"
+ not_def "~P == P-->False"
+ iff_def "P<->Q == (P-->Q) & (Q-->P)"
+
+ (* Unique existence *)
- (*Unique existence*)
-ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
+ ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
- (*Quantifiers*)
+ (* Quantifiers *)
-allI "(!!x. P(x)) ==> (ALL x.P(x))"
-spec "(ALL x.P(x)) ==> P(x)"
+ allI "(!!x. P(x)) ==> (ALL x.P(x))"
+ spec "(ALL x.P(x)) ==> P(x)"
-exI "P(x) ==> (EX x.P(x))"
-exE "[| EX x.P(x); !!x. P(x) ==> R |] ==> R"
+ exI "P(x) ==> (EX x.P(x))"
+ exE "[| EX x.P(x); !!x. P(x) ==> R |] ==> R"
(* Reflection *)
-eq_reflection "(x=y) ==> (x==y)"
-iff_reflection "(P<->Q) ==> (P==Q)"
+ eq_reflection "(x=y) ==> (x==y)"
+ iff_reflection "(P<->Q) ==> (P==Q)"
end
+