isabelle: src/FOL/IFOL.thy@1651ff6a34b5 (annotated)

1268 f6ef556b3ede corrected title clasohm parents: 928 diff changeset	1	(* Title: FOL/IFOL.thy
35 d71f96f1780e ifol.thy: added ~= for "not equals" lcp parents: 0 diff changeset	2	ID: $Id$
11677 ee12f18599e5 atomize stuff from theory FOL; wenzelm parents: 9886 diff changeset	3	Author: Lawrence C Paulson and Markus Wenzel
ee12f18599e5 atomize stuff from theory FOL; wenzelm parents: 9886 diff changeset	4	*)
35 d71f96f1780e ifol.thy: added ~= for "not equals" lcp parents: 0 diff changeset	5
11677 ee12f18599e5 atomize stuff from theory FOL; wenzelm parents: 9886 diff changeset	6	header {* Intuitionistic first-order logic *}
35 d71f96f1780e ifol.thy: added ~= for "not equals" lcp parents: 0 diff changeset	7
15481 fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 15377 diff changeset	8	theory IFOL
fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 15377 diff changeset	9	imports Pure
23155 4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	10	uses
4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	11	"~~/src/Provers/splitter.ML"
4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	12	"~~/src/Provers/hypsubst.ML"
23171 861f63a35d31 moved IsaPlanner from Provers to Tools; wenzelm parents: 23155 diff changeset	13	"~~/src/Tools/IsaPlanner/zipper.ML"
861f63a35d31 moved IsaPlanner from Provers to Tools; wenzelm parents: 23155 diff changeset	14	"~~/src/Tools/IsaPlanner/isand.ML"
861f63a35d31 moved IsaPlanner from Provers to Tools; wenzelm parents: 23155 diff changeset	15	"~~/src/Tools/IsaPlanner/rw_tools.ML"
861f63a35d31 moved IsaPlanner from Provers to Tools; wenzelm parents: 23155 diff changeset	16	"~~/src/Tools/IsaPlanner/rw_inst.ML"
23155 4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	17	"~~/src/Provers/eqsubst.ML"
4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	18	"~~/src/Provers/quantifier1.ML"
4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	19	"~~/src/Provers/project_rule.ML"
26580 c3e597a476fd Generic conversion and tactic "atomize_elim" to convert elimination rules krauss parents: 26286 diff changeset	20	"~~/src/Tools/atomize_elim.ML"
23155 4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	21	("fologic.ML")
4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	22	("hypsubstdata.ML")
4b04f9d859af proper loading of ML files; wenzelm parents: 22931 diff changeset	23	("intprover.ML")
15481 fc075ae929e4 the new subst tactic, by Lucas Dixon paulson parents: 15377 diff changeset	24	begin
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	25
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	26
11677 ee12f18599e5 atomize stuff from theory FOL; wenzelm parents: 9886 diff changeset	27	subsection {* Syntax and axiomatic basis *}
ee12f18599e5 atomize stuff from theory FOL; wenzelm parents: 9886 diff changeset	28
3906 5ae0e1324c56 global; wenzelm parents: 3835 diff changeset	29	global
5ae0e1324c56 global; wenzelm parents: 3835 diff changeset	30
14854 61bdf2ae4dc5 removed obsolete sort 'logic'; wenzelm parents: 14565 diff changeset	31	classes "term"
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	32	defaultsort "term"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	33
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	34	typedecl o
79 74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	35
11747 17a6dcd6f3cf judgment Trueprop; wenzelm parents: 11734 diff changeset	36	judgment
17a6dcd6f3cf judgment Trueprop; wenzelm parents: 11734 diff changeset	37	Trueprop :: "o => prop" ("(_)" 5)
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	38
11747 17a6dcd6f3cf judgment Trueprop; wenzelm parents: 11734 diff changeset	39	consts
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	40	True :: o
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	41	False :: o
79 74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	42
74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	43	(* Connectives *)
74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	44
17276 3bb24e8b2cb2 avoid old-style infixes; wenzelm parents: 16417 diff changeset	45	"op =" :: "['a, 'a] => o" (infixl "=" 50)
35 d71f96f1780e ifol.thy: added ~= for "not equals" lcp parents: 0 diff changeset	46
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	47	Not :: "o => o" ("~ _" [40] 40)
17276 3bb24e8b2cb2 avoid old-style infixes; wenzelm parents: 16417 diff changeset	48	"op &" :: "[o, o] => o" (infixr "&" 35)
3bb24e8b2cb2 avoid old-style infixes; wenzelm parents: 16417 diff changeset	49	"op \|" :: "[o, o] => o" (infixr "\|" 30)
3bb24e8b2cb2 avoid old-style infixes; wenzelm parents: 16417 diff changeset	50	"op -->" :: "[o, o] => o" (infixr "-->" 25)
3bb24e8b2cb2 avoid old-style infixes; wenzelm parents: 16417 diff changeset	51	"op <->" :: "[o, o] => o" (infixr "<->" 25)
79 74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	52
74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	53	(* Quantifiers *)
74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	54
7355 4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	55	All :: "('a => o) => o" (binder "ALL " 10)
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	56	Ex :: "('a => o) => o" (binder "EX " 10)
4c43090659ca proper bootstrap of IFOL/FOL theories and packages; wenzelm parents: 6340 diff changeset	57	Ex1 :: "('a => o) => o" (binder "EX! " 10)
79 74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	58
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	59
19363 667b5ea637dd refined 'abbreviation'; wenzelm parents: 19120 diff changeset	60	abbreviation
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 21210 diff changeset	61	not_equal :: "['a, 'a] => o" (infixl "~=" 50) where
19120 353d349740de not_equal: replaced syntax translation by abbreviation; wenzelm parents: 18861 diff changeset	62	"x ~= y == ~ (x = y)"
79 74e68ed3b4fd added white-space; wenzelm parents: 35 diff changeset	63
21210 c17fd2df4e9e renamed 'const_syntax' to 'notation'; wenzelm parents: 19756 diff changeset	64	notation (xsymbols)
19656 09be06943252 tuned concrete syntax -- abbreviation/const_syntax; wenzelm parents: 19380 diff changeset	65	not_equal (infixl "\<noteq>" 50)
19363 667b5ea637dd refined 'abbreviation'; wenzelm parents: 19120 diff changeset	66
21210 c17fd2df4e9e renamed 'const_syntax' to 'notation'; wenzelm parents: 19756 diff changeset	67	notation (HTML output)
19656 09be06943252 tuned concrete syntax -- abbreviation/const_syntax; wenzelm parents: 19380 diff changeset	68	not_equal (infixl "\<noteq>" 50)
19363 667b5ea637dd refined 'abbreviation'; wenzelm parents: 19120 diff changeset	69
21524 7843e2fd14a9 updated (binder) syntax/notation; wenzelm parents: 21404 diff changeset	70	notation (xsymbols)
21539 c5cf9243ad62 converted legacy ML scripts; wenzelm parents: 21524 diff changeset	71	Not ("\<not> _" [40] 40) and
c5cf9243ad62 converted legacy ML scripts; wenzelm parents: 21524 diff changeset	72	"op &" (infixr "\<and>" 35) and
c5cf9243ad62 converted legacy ML scripts; wenzelm parents: 21524 diff changeset	73	"op \|" (infixr "\<or>" 30) and
c5cf9243ad62 converted legacy ML scripts; wenzelm parents: 21524 diff changeset	74	All (binder "\<forall>" 10) and
c5cf9243ad62 converted legacy ML scripts; wenzelm parents: 21524 diff changeset	75	Ex (binder "\<exists>" 10) and
c5cf9243ad62 converted legacy ML scripts; wenzelm parents: 21524 diff changeset	76	Ex1 (binder "\<exists>!" 10) and
21524 7843e2fd14a9 updated (binder) syntax/notation; wenzelm parents: 21404 diff changeset	77	"op -->" (infixr "\<longrightarrow>" 25) and
7843e2fd14a9 updated (binder) syntax/notation; wenzelm parents: 21404 diff changeset

author	wenzelm
	Mon, 05 May 2008 15:23:59 +0200
changeset 26783	1651ff6a34b5
parent 26580	c3e597a476fd
child 26956	1309a6a0a29f
permissions	-rw-r--r--