isabelle: src/HOL/Main.thy@0263787a06b4 (annotated)

65553 006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	1	section \<open>Main HOL\<close>
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	2
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	3	text \<open>
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	4	Classical Higher-order Logic -- only ``Main'', excluding real and
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	5	complex numbers etc.
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	6	\<close>
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	7
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	8	theory Main
66817 0b12755ccbb2 euclidean rings need no normalization haftmann parents: 66614 diff changeset	9	imports
0b12755ccbb2 euclidean rings need no normalization haftmann parents: 66614 diff changeset	10	Predicate_Compile
70078 3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	11	Quickcheck_Narrowing
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 70336 diff changeset	12	Mirabelle
66817 0b12755ccbb2 euclidean rings need no normalization haftmann parents: 66614 diff changeset	13	Extraction
0b12755ccbb2 euclidean rings need no normalization haftmann parents: 66614 diff changeset	14	Nunchaku
69275 9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	15	BNF_Greatest_Fixpoint
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	16	Filter
66817 0b12755ccbb2 euclidean rings need no normalization haftmann parents: 66614 diff changeset	17	Conditionally_Complete_Lattices
0b12755ccbb2 euclidean rings need no normalization haftmann parents: 66614 diff changeset	18	Binomial
0b12755ccbb2 euclidean rings need no normalization haftmann parents: 66614 diff changeset	19	GCD
65553 006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	20	begin
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	21
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	22	subsection \<open>Namespace cleanup\<close>
69275 9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	23
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	24	hide_const (open)
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	25	czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	26	fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	27	shift proj id_bnf
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	28
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	29	hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	30
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	31
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	32	subsection \<open>Syntax cleanup\<close>
69275 9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	33
65814 3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	34	no_notation
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	35	ordLeq2 (infix "<=o" 50) and
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	36	ordLeq3 (infix "\<le>o" 50) and
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	37	ordLess2 (infix "<o" 50) and
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	38	ordIso2 (infix "=o" 50) and
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	39	card_of ("\|_\|") and
69275 9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	40	BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	41	BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	42	BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	43	BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
65814 3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	44
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	45	bundle cardinal_syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	46	begin
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	47
70078 3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	48	notation
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	49	ordLeq2 (infix "<=o" 50) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	50	ordLeq3 (infix "\<le>o" 50) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	51	ordLess2 (infix "<o" 50) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	52	ordIso2 (infix "=o" 50) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	53	card_of ("\|_\|") and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	54	BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	55	BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	56	BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	57
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	58	alias cinfinite = BNF_Cardinal_Arithmetic.cinfinite
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	59	alias czero = BNF_Cardinal_Arithmetic.czero
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	60	alias cone = BNF_Cardinal_Arithmetic.cone
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	61	alias ctwo = BNF_Cardinal_Arithmetic.ctwo
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	62
70078 3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	63	end
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	64
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	65
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	66	subsection \<open>Lattice syntax\<close>
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	67
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	68	bundle lattice_syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	69	begin
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	70
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	71	notation
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	72	bot ("\<bottom>") and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	73	top ("\<top>") and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	74	inf (infixl "\<sqinter>" 70) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	75	sup (infixl "\<squnion>" 65) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	76	Inf ("\<Sqinter> _" [900] 900) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	77	Sup ("\<Squnion> _" [900] 900)
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	78
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	79	syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	80	"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	81	"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	82	"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	83	"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	84
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	85	end
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	86
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	87	bundle no_lattice_syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	88	begin
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	89
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	90	no_notation
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	91	bot ("\<bottom>") and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	92	top ("\<top>") and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	93	inf (infixl "\<sqinter>" 70) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	94	sup (infixl "\<squnion>" 65) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	95	Inf ("\<Sqinter> _" [900] 900) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	96	Sup ("\<Squnion> _" [900] 900)
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	97
65814 3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	98	no_syntax
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	99	"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	100	"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	101	"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	102	"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	103
65553 006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	104	end
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	105
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	106	unbundle no_lattice_syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	107
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	108	end

author	paulson <lp15@cam.ac.uk>
	Sat, 04 Dec 2021 20:30:16 +0000
changeset 74878	0263787a06b4
parent 74337	9c1ad2f04660
child 76224	64e8d4afcf10
permissions	-rw-r--r--