isabelle: src/HOL/Main.thy@3e11f510b3f6 (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
76224 64e8d4afcf10 moved relevant theorems from theory Divides to theory Euclidean_Division haftmann parents: 74337 diff changeset	20	Divides
65553 006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	21	begin
006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	22
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	23	subsection \<open>Namespace cleanup\<close>
69275 9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	24
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	25	hide_const (open)
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	26	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	27	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	28	shift proj id_bnf
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	29
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	30	hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	31
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	32
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	33	subsection \<open>Syntax cleanup\<close>
69275 9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	34
65814 3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	35	no_notation
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	36	ordLeq2 (infix "<=o" 50) and
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	37	ordLeq3 (infix "\<le>o" 50) and
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	38	ordLess2 (infix "<o" 50) and
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	39	ordIso2 (infix "=o" 50) and
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	40	card_of ("\|_\|") and
69275 9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	41	BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	42	BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	43	BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and
9bbd5497befd clarified status of legacy input abbreviations haftmann parents: 68980 diff changeset	44	BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
65814 3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	45
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	46	bundle cardinal_syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	47	begin
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	48
70078 3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	49	notation
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	50	ordLeq2 (infix "<=o" 50) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	51	ordLeq3 (infix "\<le>o" 50) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	52	ordLess2 (infix "<o" 50) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	53	ordIso2 (infix "=o" 50) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	54	card_of ("\|_\|") and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	55	BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	56	BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	57	BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	58
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	59	alias cinfinite = BNF_Cardinal_Arithmetic.cinfinite
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	60	alias czero = BNF_Cardinal_Arithmetic.czero
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	61	alias cone = BNF_Cardinal_Arithmetic.cone
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	62	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	63
70078 3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	64	end
3a1b2d8c89aa bundle for cardinal syntax traytel parents: 69745 diff changeset	65
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	66
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	67	subsection \<open>Lattice syntax\<close>
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	68
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	69	bundle lattice_syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	70	begin
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	71
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	72	notation
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	73	bot ("\<bottom>") and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	74	top ("\<top>") and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	75	inf (infixl "\<sqinter>" 70) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	76	sup (infixl "\<squnion>" 65) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	77	Inf ("\<Sqinter> _" [900] 900) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	78	Sup ("\<Squnion> _" [900] 900)
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	79
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	80	syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	81	"_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	82	"_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	83	"_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	84	"_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	85
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	86	end
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	87
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	88	bundle no_lattice_syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	89	begin
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	90
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	91	no_notation
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	92	bot ("\<bottom>") and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	93	top ("\<top>") and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	94	inf (infixl "\<sqinter>" 70) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	95	sup (infixl "\<squnion>" 65) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	96	Inf ("\<Sqinter> _" [900] 900) and
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	97	Sup ("\<Squnion> _" [900] 900)
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	98
65814 3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	99	no_syntax
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	100	"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	101	"_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	102	"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
3039d4aa7143 obsolete (see also bdd17b18e103, f533820e7248); wenzelm parents: 65813 diff changeset	103	"_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	104
65553 006a274cdbc2 added missing file (amending f533820e7248); wenzelm parents: diff changeset	105	end
74334 ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	106
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	107	unbundle no_lattice_syntax
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	108
ead56ad40e15 bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax; wenzelm parents: 74102 diff changeset	109	end

author	wenzelm
	Wed, 05 Jul 2023 15:01:46 +0200
changeset 78255	3e11f510b3f6
parent 76224	64e8d4afcf10
child 80453	7a2d9e3fcdd5
permissions	-rw-r--r--